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

Theorem ax15 2104
Description: Axiom ax-15 2105 is redundant if we assume ax-17 1628. 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 2102 and ax-17 1628. By the end of the proof it has vanished, and the final theorem has no distinct variable requirements.

This theorem should not be referenced in any proof. Instead, use ax-15 2105 below so that theorems needing ax-15 2105 can be more easily identified. (Contributed by NM, 29-Jun-1995.) (Proof modification is discouraged.) (New usage 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
StepHypRef Expression
1 hbn1 1564 . . . . 5  |-  ( -. 
A. z  z  =  y  ->  A. z  -.  A. z  z  =  y )
2 dveel2 2102 . . . . 5  |-  ( -. 
A. z  z  =  y  ->  ( w  e.  y  ->  A. z  w  e.  y )
)
31, 2hbim1 1810 . . . 4  |-  ( ( -.  A. z  z  =  y  ->  w  e.  y )  ->  A. z
( -.  A. z 
z  =  y  ->  w  e.  y )
)
4 ax-17 1628 . . . 4  |-  ( ( -.  A. z  z  =  y  ->  x  e.  y )  ->  A. w
( -.  A. z 
z  =  y  ->  x  e.  y )
)
5 elequ1 1831 . . . . 5  |-  ( w  =  x  ->  (
w  e.  y  <->  x  e.  y ) )
65imbi2d 309 . . . 4  |-  ( w  =  x  ->  (
( -.  A. z 
z  =  y  ->  w  e.  y )  <->  ( -.  A. z  z  =  y  ->  x  e.  y ) ) )
73, 4, 6dvelimfALT 1854 . . 3  |-  ( -. 
A. z  z  =  x  ->  ( ( -.  A. z  z  =  y  ->  x  e.  y )  ->  A. z
( -.  A. z 
z  =  y  ->  x  e.  y )
) )
8 nfa1 1719 . . . . 5  |-  F/ z A. z  z  =  y
98nfn 1731 . . . 4  |-  F/ z  -.  A. z  z  =  y
10919.21 1771 . . 3  |-  ( A. z ( -.  A. z  z  =  y  ->  x  e.  y )  <-> 
( -.  A. z 
z  =  y  ->  A. z  x  e.  y ) )
117, 10syl6ib 219 . 2  |-  ( -. 
A. z  z  =  x  ->  ( ( -.  A. z  z  =  y  ->  x  e.  y )  ->  ( -.  A. z  z  =  y  ->  A. z  x  e.  y )
) )
1211pm2.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 1532    = wceq 1619    e. wcel 1621
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540
  Copyright terms: Public domain W3C validator