Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ax-15 Unicode version

Axiom ax-15 2102
 Description: Axiom of Quantifier Introduction. One of the equality and substitution axioms for a non-logical predicate in our predicate calculus with equality. Axiom scheme C14' in [Megill] p. 448 (p. 16 of the preprint). It is redundant if we include ax-17 1628; see theorem ax15 2101. Alternately, ax-17 1628 becomes unnecessary in principle with this axiom, but we lose the more powerful metalogic afforded by ax-17 1628. We retain ax-15 2102 here to provide completeness for systems with the simpler metalogic that results from omitting ax-17 1628, which might be easier to study for some theoretical purposes. (Contributed by NM, 5-Aug-1993.) (New usage is discouraged.)
Assertion
Ref Expression
ax-15

Detailed syntax breakdown of Axiom ax-15
StepHypRef Expression
1 vz . . . . 5
2 vx . . . . 5
31, 2weq 1620 . . . 4
43, 1wal 1532 . . 3
54wn 5 . 2
6 vy . . . . . 6
71, 6weq 1620 . . . . 5
87, 1wal 1532 . . . 4
98wn 5 . . 3
102, 6wel 1622 . . . 4
1110, 1wal 1532 . . . 4
1210, 11wi 6 . . 3
139, 12wi 6 . 2
145, 13wi 6 1
 Colors of variables: wff set class This axiom is referenced by:  ax17el  2103  ax11el  2106
 Copyright terms: Public domain W3C validator