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

Theorem ax15 1974
Description: Axiom ax-15 2095 is redundant if we assume ax-17 1606. Remark 9.6 in [Megill] p. 448 (p. 16 of the preprint), regarding axiom scheme C14'.

Note that  w is a dummy variable introduced in the proof. On the web page, it is implicitly assumed to be distinct from all other variables. (This is made explicit in the database file set.mm). Its purpose is to satisfy the distinct variable requirements of dveel2 1973 and ax-17 1606. By the end of the proof it has vanished, and the final theorem has no distinct variable requirements. (Contributed by NM, 29-Jun-1995.) (Proof modification is discouraged.)

Assertion
Ref Expression
ax15  |-  ( -. 
A. z  z  =  x  ->  ( -.  A. z  z  =  y  ->  ( x  e.  y  ->  A. z  x  e.  y )
) )

Proof of Theorem ax15
Dummy variable  w is distinct from all other variables.
StepHypRef Expression
1 hbn1 1716 . . . . 5  |-  ( -. 
A. z  z  =  y  ->  A. z  -.  A. z  z  =  y )
2 dveel2 1973 . . . . 5  |-  ( -. 
A. z  z  =  y  ->  ( w  e.  y  ->  A. z  w  e.  y )
)
31, 2hbim1 1744 . . . 4  |-  ( ( -.  A. z  z  =  y  ->  w  e.  y )  ->  A. z
( -.  A. z 
z  =  y  ->  w  e.  y )
)
4 elequ1 1699 . . . . 5  |-  ( w  =  x  ->  (
w  e.  y  <->  x  e.  y ) )
54imbi2d 307 . . . 4  |-  ( w  =  x  ->  (
( -.  A. z 
z  =  y  ->  w  e.  y )  <->  ( -.  A. z  z  =  y  ->  x  e.  y ) ) )
63, 5dvelim 1969 . . 3  |-  ( -. 
A. z  z  =  x  ->  ( ( -.  A. z  z  =  y  ->  x  e.  y )  ->  A. z
( -.  A. z 
z  =  y  ->  x  e.  y )
) )
7 nfa1 1768 . . . . 5  |-  F/ z A. z  z  =  y
87nfn 1777 . . . 4  |-  F/ z  -.  A. z  z  =  y
9819.21 1803 . . 3  |-  ( A. z ( -.  A. z  z  =  y  ->  x  e.  y )  <-> 
( -.  A. z 
z  =  y  ->  A. z  x  e.  y ) )
106, 9syl6ib 217 . 2  |-  ( -. 
A. z  z  =  x  ->  ( ( -.  A. z  z  =  y  ->  x  e.  y )  ->  ( -.  A. z  z  =  y  ->  A. z  x  e.  y )
) )
1110pm2.86d 93 1  |-  ( -. 
A. z  z  =  x  ->  ( -.  A. z  z  =  y  ->  ( x  e.  y  ->  A. z  x  e.  y )
) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4   A.wal 1530
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535
  Copyright terms: Public domain W3C validator