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

Theorem ax15 1968
Description: Axiom ax-15 2087 is redundant if we assume ax-17 1605. 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 1967 and ax-17 1605. 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 )
) )
Dummy variable  w is distinct from all other variables.

Proof of Theorem ax15
StepHypRef Expression
1 hbn1 1707 . . . . 5  |-  ( -. 
A. z  z  =  y  ->  A. z  -.  A. z  z  =  y )
2 dveel2 1967 . . . . 5  |-  ( -. 
A. z  z  =  y  ->  ( w  e.  y  ->  A. z  w  e.  y )
)
31, 2hbim1 1736 . . . 4  |-  ( ( -.  A. z  z  =  y  ->  w  e.  y )  ->  A. z
( -.  A. z 
z  =  y  ->  w  e.  y )
)
4 elequ1 1690 . . . . 5  |-  ( w  =  x  ->  (
w  e.  y  <->  x  e.  y ) )
54imbi2d 309 . . . 4  |-  ( w  =  x  ->  (
( -.  A. z 
z  =  y  ->  w  e.  y )  <->  ( -.  A. z  z  =  y  ->  x  e.  y ) ) )
63, 5dvelim 1963 . . 3  |-  ( -. 
A. z  z  =  x  ->  ( ( -.  A. z  z  =  y  ->  x  e.  y )  ->  A. z
( -.  A. z 
z  =  y  ->  x  e.  y )
) )
7 nfa1 1760 . . . . 5  |-  F/ z A. z  z  =  y
87nfn 1769 . . . 4  |-  F/ z  -.  A. z  z  =  y
9819.21 1795 . . 3  |-  ( A. z ( -.  A. z  z  =  y  ->  x  e.  y )  <-> 
( -.  A. z 
z  =  y  ->  A. z  x  e.  y ) )
106, 9syl6ib 219 . 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 5    -> wi 6   A.wal 1529
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1638  ax-8 1646  ax-13 1689  ax-14 1691  ax-6 1706  ax-7 1711  ax-11 1718  ax-12 1870
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1312  df-ex 1531  df-nf 1534
  Copyright terms: Public domain W3C validator