MPE Home 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  |-  ( -. 
A. z  z  =  x  ->  ( -.  A. z  z  =  y  ->  ( x  e.  y  ->  A. z  x  e.  y )
) )

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