50. ⊢[A(a) → B(b, c, ...)] ⇒ ⊢[(∃x)Ax → B] provided that 'a' doesn't occur in the wff 'B'

'Rule C / Existential instantiation' (Th. 1804 of MM)

51. ⊢ (∃x)(x = a) 'at least one thing exist' (alternate form of Ax. 8) (Th. 1835 of MM)

52. ⊢A(a) ⇒ ⊢((∃x)A[x/a]) 'Existential generalization' (Th. 1836 of MM)

53. ⊢ (∀x)Ax → (∃x)Ax (Th. 1837 of MM)

54. ⊢ [(∃x)Ax → (∃x)Bx] → (∃x)(Ax → Bx) (Th. 1844 of MM)

55. ⊢ x = x 'Identity 2' (Th. 1884 of MM)

56. ⊢ (x = y) ↔︎ (y = x) 'Commutativity of identity' (Th. 1891 of MM)

57. ⊢ (x = y) → [(x = z) ↔︎ (y = z)] 'Transitivity of identity' (Th. 1898 MM)

58. ⊢ (∀x)(x = x) 'Reflexivity of identity' (one of the usual axioms of a first-order logic textbook) (Th. 1903 of MM)

59. ⊢ (x = y) → (𝜑(x) → 𝜑[y/x]) 'Substitutivity of identity' (a "textbook" axiom) (Th. 1904 of MM)

Theorems requiring only Axioms 1 - 13 and the auxiliary Axioms 20 - 24

60. ⊢ A(a) → (∃x)A[x/a] (Th. 1985 of MM)

61. ⊢ (∀x)A(x) → A[a/x] 'Universal instantiation' (a "textbook" axiom) (Th. 2232 of MM)

62. ⊢(Ⅎx)A(x) ⇒ ⊢[(∀x)(A(x) → B(x)) → (A(x) → (∀x)Bx)] (a "textbook" axiom) (Th. 2040 of MM)

63. ⊢ (∃x)(∀y)A[x, y] → (∀y)(∃x)A[x, y] 'if there is an x such that for all y, A is true, then for all y there is an x such that A is true' (the converse doesn't always hold) (Th. 2082 of MM)

Example: If there is someone who loves everyone, then everyone is loved by someone.

Its converse doesn't hold: It is false that, if everyone is loved by someone, then there is someone who loves everyone (because there might be two or more lovers who don't love the same person as each other does.)

64. ⊢(∀x)A(x) ⇒ ⊢A[a/x] 'Universal instantiation' (Th. 1992 of MM)

65. ⊢(∀x)(Ax → Bx) , ⊢(∀x)(Bx → Cx) ⇒ ⊢(∀x)(Ax → Cx) 'Universal hypothetical syllogism / Barbara' (Aristotle's syllogism) (Th. 2442 of MM)

66. ⊢(∀x)(Ax → Bx) , ⊢(∃x)(Cx & Ax) ⇒ ⊢(∃x)(Cx & Bx) 'Darii' (Aristotle's syllogism) (Th. 2444 of MM)

67. ⊢(∀x)(Ax → Bx) , ⊢(∀x)(Cx → Ax) ⇒ ⊢[(∃x)Cx → (∃x)Bx)] 'Barbari w/o existential import' (Aristotle's syllogism)

1. (∀x)(Ax → Bx) (H1)

2. (∀x)(Cx → Ax) (H2)

3. (∀x)(Cx → Bx) (2, 1, th.65)

4. (∀x)(Cx → Bx) → [(∃x)Cx → (∃x)Bx] (Th. 1734 of MM)

5. (∃x)Cx → (∃x)Bx (3, 4 MP) QED

68. ⊢(∀x)(Ax → Bx) , ⊢(∀x)(Ax → Cx) ⇒ ⊢[(∃x)Ax → (∃x)(Cx & Bx)] 'Darapti w/o existential import' (Aristotle's syllogism)

1. (∀x)(Ax → Bx) (H1)

2. (∀x)(Ax → Cx) (H2)

3. Aa → Ba (1, ∀I th.65)

4. Aa → Ca (2, ∀I)

5. Aa → (Ca & Ba) (3, 4, Th. 546 of MM)

6. (∃x)Ax → (∃x)(Cx & Bx) (5, th.46) QED

69. ⊢ (∃x)(∃y)A[x, y] ↔︎ (∃y)(∃x)A[x, y] 'Commutability of existential quantifier' (Th. 1974 of MM)

70. ⊢ ¬(∀x)Ax → (∀x)¬(∀x)Ax (Axiom 10 of MM)

1. (Ⅎx)[¬(∀x)Ax] (Ax. 20)

2. (Ⅎx)[¬(∀x)Ax] ≝ (∀x)[¬(∀x)Ax → (∀x)¬(∀x)Ax] (def. of (Ⅎx)A)

3. (Ⅎx)[¬(∀x)Ax] → (∀x)[¬(∀x)Ax → (∀x)¬(∀x)Ax] (2, th.3)

4. (∀x)[¬(∀x)Ax → (∀x)¬(∀x)Ax] (1, 3 MP)

5. ¬(∀x)Ax → (∀x)¬(∀x)Ax (4, ∀I) QED

Inference theorems for facilitating proofs:

71. ⊢¬¬A ⇔ ⊢A 'Double negation introduction/elimination' (Th. 114/123 of MM)

72. ⊢A , ⊢(A ↔︎ B) ⇒ ⊢B 'Biconditional modus ponens' (Th. 208 of MM)

73. ⊢(A → B) ⇔ ⊢(¬A ∨ B) 'Conditional exchange' (Th. 413/414 of MM)

74. ⊢[(A & B) → C] ⇔ ⊢[A → (B → C)] 'Importation-exportation' (Th. 429/434 of MM)

75. ⊢¬(A & B) ⇔ ⊢(¬A ∨ ¬B) 'De Morgan's law 1'

1. ¬(A & B) (H)

   1. ¬(A & B) ↔︎ (¬A ∨ ¬B) (th.22)

   2. (¬A ∨ ¬B) (1, 1.1, th. 72)

1. (¬A ∨ ¬B) (H)

   1. ¬(A & B) ↔︎ (¬A ∨ ¬B) (th.22)

   2. ¬(A & B) (1, 1.1, th. 72) QED

76. ⊢¬(A ∨ B) ⇔ ⊢(¬A & ¬B) 'De Morgan's law 2' (similar proof to that of Th. 73 but utilizing Th. 23 instead of Th. 22)

77. ⊢(∀x)¬Px ⇔ ⊢¬(∃x)Px (Similar proof using Th. 38)

78. ⊢(∀x)Px ⇔ ⊢¬(∃x)¬Px (Similar proof using Th. 39)

79. ⊢(∃x)¬Px ⇔ ⊢¬(∀x)Px (Similar proof using Th. 40)

80. ⊢(A ≝ B) , ⊢A ⇒ ⊢B 'Definition'

1. A ≝ B (H1)

2. A (H2)

3. A → B (1, th. 3)

4. B (2, 3, MP) QED

Theorems requiring all 24 non-modal axioms

81. ⊢(∀*x ∈ A)(x ∈ B), ⊢(∀*x ∈ C)(x ∈ A) ⇒ ⊢(∃x)[(x ∈ C) & (x ∈ B)] 'Barbari' (Aristotle's syllogism)

1. (∀*x ∈ A)(x ∈ B) (H1)

2. (∀*x ∈ C)(x ∈ A) (H2)

3. (∀*x ∈ A)(x ∈ B) ≝ [(∀x)[(x ∈ A) → (x ∈ B)] & (∃x)(x ∈ A)] (def. of natural restricted quantification)

4. (∀*x ∈ C)(x ∈ A) ≝ [(∀x)[(x ∈ C) → (x ∈ A)] & (∃x)(x ∈ C)] (def. of natural restricted quantification)

5. (∀x)[(x ∈ A) → (x ∈ B)] & (∃x)(x ∈ A)] (1, 3, th.80)

6. (∀x)[(x ∈ C) → (x ∈ A)] & (∃x)(x ∈ C)] (2, 4, th.80)

7. (∃x)(x ∈ C) (6, &-elim)

8. (∀x)[(x ∈ A) → (x ∈ B)] (5, &-elim.)

9. (∀x)[(x ∈ C) → (x ∈ A)] (5, &-elim.)

10. (∀x)[(x ∈ C) → (x ∈ B)] (8, 9, th.65)

11. (a ∈ C) → (a ∈ B) (10, ∀I)

12. (a ∈ C) → [(a ∈ C) & (a ∈ B)] (11, Th .565 of MM)

13. (∃x)(x ∈ C) → (∃x)[(x ∈ C) & (x ∈ B)] (12, th.46)

14. (∃x)[(x ∈ C) & (x ∈ B)] (7, 13 MP) QED

82. ⊢(∀*x ∈ A)(x ∈ B) , ⊢(∀*x ∈ A)(x ∈ C) ⇒ ⊢(∃x)[(x ∈ C) & (x ∈ B)] 'Darapti' (Aristotle's syllogism)

1. (∀*x ∈ A)(x ∈ B) (H1)

2. (∀*x ∈ A)(x ∈ C) (H2)

3. (∀*x ∈ A)(x ∈ B) ≝ [(∀x)[(x ∈ A) → (x ∈ B)] & (∃x)(x ∈ A)] (def. of natural restricted quantification)

4. (∀*x ∈ A)(x ∈ C) ≝ [(∀x)[(x ∈ A) → (x ∈ C)] & (∃x)(x ∈ A)] (def. of natural restricted quantification)

5. (∀x)[(x ∈ A) → (x ∈ B)] & (∃x)(x ∈ A)] (1, 3, th.80)

6. (∀x)[(x ∈ A) → (x ∈ C)] & (∃x)(x ∈ A)] (2, 4, th.80)

7. (∃x)(x ∈ A) (5, &-elim)

8. (∀x)[(x ∈ A) → (x ∈ B)] (5, &-elim.)

9. (∀x)[(x ∈ A) → (x ∈ C)] (6, &-elim.)

10. (a ∈ A) → (a ∈ B) (8, ∀I)

11. (a ∈ A) → (a ∈ C) (9, ∀I)

12. (a ∈ A) → [(a ∈ C) & (a ∈ B)] (10, 11, Th. 546 of MM)

13. (∃x)(x ∈ A) → (∃x)[(x ∈ C) & (x ∈ B)] (12, th.46)

14. (∃x)[(x ∈ C) & (x ∈ B)] (7, 13 MP) QED

83. ⊢ [A = B] ↔︎ (∀x)[(x ∈ A) ↔︎ (x ∈ B)] 'Set identity' (Th. 2495 of MM)

84. ⊢ A ∉ A 'Irreflexivity of set membership' (no set contains itself) (Th. 8181 of MM)

From this point onwards, every symbol and formula used in mathematics are wffs of L1+ZF and their textbook definitions are imported.

85. ⊢A[0/x] , ⊢[(x ∈ N) → (A → A[(x+1)/x]) ] ⇒ ⊢[(x ∈ N) → A], where N is the set of natural numbers. 'Mathematical induction' (Th. 6785 of MM)