Type  Label  Description 
Statement 

Theorem  exnal 201* 
Theorem 19.14 of [Margaris] p. 90.
(Contributed by Mario Carneiro,
10Oct2014.)



Axiom  axinf 202 
The axiom of infinity: the set of "individuals" is not
Dedekindfinite.
Using the axiom of choice, we can show that this is equivalent to an
embedding of the natural numbers in . (Contributed by Mario
Carneiro, 10Oct2014.)

11
onto 

0.6 Rederive the Metamath
axioms


Theorem  ax1 203 
Axiom Simp. Axiom A1 of [Margaris] p.
49. (Contributed by Mario
Carneiro, 9Oct2014.)



Theorem  ax2 204 
Axiom Frege. Axiom A2 of [Margaris]
p. 49. (Contributed by Mario
Carneiro, 9Oct2014.)



Theorem  ax3 205 
Axiom Transp. Axiom A3 of [Margaris]
p. 49. (Contributed by Mario
Carneiro, 10Oct2014.)



Theorem  axmp 206 
Rule of Modus Ponens. The postulated inference rule of propositional
calculus. See e.g. Rule 1 of [Hamilton] p. 73. (Contributed by Mario
Carneiro, 10Oct2014.)



Theorem  ax5 207* 
Axiom of Quantified Implication. Axiom C4 of [Monk2] p. 105.
(Contributed by Mario Carneiro, 10Oct2014.)



Theorem  ax6 208* 
Axiom of Quantified Negation. Axiom C52 of [Monk2] p. 113.
(Contributed by Mario Carneiro, 10Oct2014.)



Theorem  ax7 209* 
Axiom of Quantifier Commutation. Axiom scheme C6' in [Megill] p. 448
(p. 16 of the preprint). (Contributed by Mario Carneiro,
10Oct2014.)



Theorem  axgen 210* 
Rule of Generalization. See e.g. Rule 2 of [Hamilton] p. 74.
(Contributed by Mario Carneiro, 10Oct2014.)



Theorem  ax8 211 
Axiom of Equality. Axiom scheme C8' in [Megill] p. 448 (p. 16 of the
preprint). Also appears as Axiom C7 of [Monk2] p. 105. (Contributed by
Mario Carneiro, 10Oct2014.)



Theorem  ax9 212* 
Axiom of Equality. Axiom scheme C8' in [Megill] p. 448 (p. 16 of the
preprint). Also appears as Axiom C7 of [Monk2] p. 105. (Contributed by
Mario Carneiro, 10Oct2014.)



Theorem  ax10 213* 
Axiom of Quantifier Substitution. Appears as Lemma L12 in [Megill]
p. 445 (p. 12 of the preprint). (Contributed by Mario Carneiro,
10Oct2014.)



Theorem  ax11 214* 
Axiom of Variable Substitution. It is based on Lemma 16 of [Tarski]
p. 70 and Axiom C8 of [Monk2] p. 105,
from which it can be proved by
cases. (Contributed by Mario Carneiro, 10Oct2014.)



Theorem  ax12 215* 
Axiom of Quantifier Introduction. Axiom scheme C9' in [Megill] p. 448
(p. 16 of the preprint). (Contributed by Mario Carneiro,
10Oct2014.)



Theorem  ax13 216 
Axiom of Equality. Axiom scheme C12' in [Megill] p. 448 (p. 16 of the
preprint). It is a special case of Axiom B8 (p. 75) of system S2 of
[Tarski] p. 77. (Contributed by Mario
Carneiro, 10Oct2014.)



Theorem  ax14 217 
Axiom of Equality. Axiom scheme C12' in [Megill] p. 448 (p. 16 of the
preprint). It is a special case of Axiom B8 (p. 75) of system S2 of
[Tarski] p. 77. (Contributed by Mario
Carneiro, 10Oct2014.)



Theorem  ax17m 218* 
Axiom to quantify a variable over a formula in which it does not occur.
Axiom C5 in [Megill] p. 444 (p. 11 of
the preprint). Also appears as
Axiom B6 (p. 75) of system S2 of [Tarski] p. 77 and Axiom C51 of
[Monk2] p. 113. (Contributed by Mario
Carneiro, 10Oct2014.)



Theorem  axext 219* 
Axiom of Extensionality. An axiom of ZermeloFraenkel set theory. It
states that two sets are identical if they contain the same elements.
Axiom Ext of [BellMachover] p.
461. (Contributed by Mario Carneiro,
10Oct2014.)



Theorem  axrep 220* 
Axiom of Replacement. An axiom scheme of ZermeloFraenkel set theory.
Axiom 5 of [TakeutiZaring] p. 19.
(Contributed by Mario Carneiro,
10Oct2014.)



Theorem  axpow 221* 
Axiom of Power Sets. An axiom of ZermeloFraenkel set theory.
(Contributed by Mario Carneiro, 10Oct2014.)



Theorem  axun 222* 
Axiom of Union. An axiom of ZermeloFraenkel set theory. (Contributed
by Mario Carneiro, 10Oct2014.)

