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

Theorem ax15 2070
Description: Axiom ax-15 2193 is redundant if we assume ax-17 1623. 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 2069 and ax-17 1623. 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 1741 . . . . 5  |-  ( -. 
A. z  z  =  y  ->  A. z  -.  A. z  z  =  y )
2 dveel2 2069 . . . . 5  |-  ( -. 
A. z  z  =  y  ->  ( w  e.  y  ->  A. z  w  e.  y )
)
31, 2hbim1 1825 . . . 4  |-  ( ( -.  A. z  z  =  y  ->  w  e.  y )  ->  A. z
( -.  A. z 
z  =  y  ->  w  e.  y )
)
4 elequ1 1724 . . . . 5  |-  ( w  =  x  ->  (
w  e.  y  <->  x  e.  y ) )
54imbi2d 308 . . . 4  |-  ( w  =  x  ->  (
( -.  A. z 
z  =  y  ->  w  e.  y )  <->  ( -.  A. z  z  =  y  ->  x  e.  y ) ) )
63, 5dvelim 2066 . . 3  |-  ( -. 
A. z  z  =  x  ->  ( ( -.  A. z  z  =  y  ->  x  e.  y )  ->  A. z
( -.  A. z 
z  =  y  ->  x  e.  y )
) )
7 nfa1 1802 . . . . 5  |-  F/ z A. z  z  =  y
87nfn 1807 . . . 4  |-  F/ z  -.  A. z  z  =  y
9819.21 1810 . . 3  |-  ( A. z ( -.  A. z  z  =  y  ->  x  e.  y )  <-> 
( -.  A. z 
z  =  y  ->  A. z  x  e.  y ) )
106, 9syl6ib 218 . 2  |-  ( -. 
A. z  z  =  x  ->  ( ( -.  A. z  z  =  y  ->  x  e.  y )  ->  ( -.  A. z  z  =  y  ->  A. z  x  e.  y )
) )
1110pm2.86d 95 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 1546
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator