Users' Mathboxes Mathbox for Andrew Salmon < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ax10ext Unicode version

Theorem ax10ext 27709
Description: This theorem shows that, given axext4 2280, we can derive a version of ax10 1897. However, it is weaker than ax10 1897 because it has a distinct variable requirement. (Contributed by Andrew Salmon, 16-Jul-2011.) (Proof modification is discouraged.)
Assertion
Ref Expression
ax10ext  |-  ( A. x  x  =  z  ->  A. z  z  =  x )
Distinct variable group:    x, z

Proof of Theorem ax10ext
Dummy variable  w is distinct from all other variables.
StepHypRef Expression
1 ax-ext 2277 . . . . . 6  |-  ( A. w ( w  e.  x  <->  w  e.  z
)  ->  x  =  z )
21alimi 1549 . . . . 5  |-  ( A. x A. w ( w  e.  x  <->  w  e.  z )  ->  A. x  x  =  z )
3 ax-7 1720 . . . . . . 7  |-  ( A. x A. w ( w  e.  x  <->  w  e.  z )  ->  A. w A. x ( w  e.  x  <->  w  e.  z
) )
4 ax-14 1700 . . . . . . . . 9  |-  ( x  =  z  ->  (
w  e.  x  ->  w  e.  z )
)
5 bi2 189 . . . . . . . . . . 11  |-  ( ( w  e.  x  <->  w  e.  z )  ->  (
w  e.  z  ->  w  e.  x )
)
65alimi 1549 . . . . . . . . . 10  |-  ( A. x ( w  e.  x  <->  w  e.  z
)  ->  A. x
( w  e.  z  ->  w  e.  x
) )
7 nfv 1609 . . . . . . . . . . 11  |-  F/ x  w  e.  z
87stdpc5 1805 . . . . . . . . . 10  |-  ( A. x ( w  e.  z  ->  w  e.  x )  ->  (
w  e.  z  ->  A. x  w  e.  x ) )
96, 8syl 15 . . . . . . . . 9  |-  ( A. x ( w  e.  x  <->  w  e.  z
)  ->  ( w  e.  z  ->  A. x  w  e.  x )
)
104, 9syl9 66 . . . . . . . 8  |-  ( x  =  z  ->  ( A. x ( w  e.  x  <->  w  e.  z
)  ->  ( w  e.  x  ->  A. x  w  e.  x )
) )
1110alimdv 1611 . . . . . . 7  |-  ( x  =  z  ->  ( A. w A. x ( w  e.  x  <->  w  e.  z )  ->  A. w
( w  e.  x  ->  A. x  w  e.  x ) ) )
123, 11syl5 28 . . . . . 6  |-  ( x  =  z  ->  ( A. x A. w ( w  e.  x  <->  w  e.  z )  ->  A. w
( w  e.  x  ->  A. x  w  e.  x ) ) )
1312sps 1751 . . . . 5  |-  ( A. x  x  =  z  ->  ( A. x A. w ( w  e.  x  <->  w  e.  z
)  ->  A. w
( w  e.  x  ->  A. x  w  e.  x ) ) )
142, 13mpcom 32 . . . 4  |-  ( A. x A. w ( w  e.  x  <->  w  e.  z )  ->  A. w
( w  e.  x  ->  A. x  w  e.  x ) )
1514a5i 1770 . . 3  |-  ( A. x A. w ( w  e.  x  <->  w  e.  z )  ->  A. x A. w ( w  e.  x  ->  A. x  w  e.  x )
)
16 nfa1 1768 . . . . . . . 8  |-  F/ x A. x  w  e.  x
171619.23 1809 . . . . . . 7  |-  ( A. x ( w  e.  x  ->  A. x  w  e.  x )  <->  ( E. x  w  e.  x  ->  A. x  w  e.  x )
)
18 19.8a 1730 . . . . . . . . 9  |-  ( w  e.  z  ->  E. z  w  e.  z )
19 elequ2 1701 . . . . . . . . . 10  |-  ( z  =  x  ->  (
w  e.  z  <->  w  e.  x ) )
2019cbvexv 1956 . . . . . . . . 9  |-  ( E. z  w  e.  z  <->  E. x  w  e.  x )
2118, 20sylib 188 . . . . . . . 8  |-  ( w  e.  z  ->  E. x  w  e.  x )
22 nfv 1609 . . . . . . . . 9  |-  F/ z  w  e.  x
2322, 7, 4cbv3 1935 . . . . . . . 8  |-  ( A. x  w  e.  x  ->  A. z  w  e.  z )
2421, 23imim12i 53 . . . . . . 7  |-  ( ( E. x  w  e.  x  ->  A. x  w  e.  x )  ->  ( w  e.  z  ->  A. z  w  e.  z ) )
2517, 24sylbi 187 . . . . . 6  |-  ( A. x ( w  e.  x  ->  A. x  w  e.  x )  ->  ( w  e.  z  ->  A. z  w  e.  z ) )
2625alimi 1549 . . . . 5  |-  ( A. w A. x ( w  e.  x  ->  A. x  w  e.  x )  ->  A. w ( w  e.  z  ->  A. z  w  e.  z )
)
2726a7s 1721 . . . 4  |-  ( A. x A. w ( w  e.  x  ->  A. x  w  e.  x )  ->  A. w ( w  e.  z  ->  A. z  w  e.  z )
)
2827alrimiv 1621 . . 3  |-  ( A. x A. w ( w  e.  x  ->  A. x  w  e.  x )  ->  A. z A. w
( w  e.  z  ->  A. z  w  e.  z ) )
29 nfa1 1768 . . . . . . . 8  |-  F/ z A. z  w  e.  z
302919.23 1809 . . . . . . 7  |-  ( A. z ( w  e.  z  ->  A. z  w  e.  z )  <->  ( E. z  w  e.  z  ->  A. z  w  e.  z )
)
31 ax-14 1700 . . . . . . . . . 10  |-  ( z  =  x  ->  (
w  e.  z  ->  w  e.  x )
)
3231spimv 1943 . . . . . . . . 9  |-  ( A. z  w  e.  z  ->  w  e.  x )
3318, 32imim12i 53 . . . . . . . 8  |-  ( ( E. z  w  e.  z  ->  A. z  w  e.  z )  ->  ( w  e.  z  ->  w  e.  x
) )
34 19.8a 1730 . . . . . . . . . 10  |-  ( w  e.  x  ->  E. x  w  e.  x )
35 elequ2 1701 . . . . . . . . . . 11  |-  ( x  =  z  ->  (
w  e.  x  <->  w  e.  z ) )
3635cbvexv 1956 . . . . . . . . . 10  |-  ( E. x  w  e.  x  <->  E. z  w  e.  z )
3734, 36sylib 188 . . . . . . . . 9  |-  ( w  e.  x  ->  E. z  w  e.  z )
38 sp 1728 . . . . . . . . 9  |-  ( A. z  w  e.  z  ->  w  e.  z )
3937, 38imim12i 53 . . . . . . . 8  |-  ( ( E. z  w  e.  z  ->  A. z  w  e.  z )  ->  ( w  e.  x  ->  w  e.  z ) )
4033, 39impbid 183 . . . . . . 7  |-  ( ( E. z  w  e.  z  ->  A. z  w  e.  z )  ->  ( w  e.  z  <-> 
w  e.  x ) )
4130, 40sylbi 187 . . . . . 6  |-  ( A. z ( w  e.  z  ->  A. z  w  e.  z )  ->  ( w  e.  z  <-> 
w  e.  x ) )
4241alimi 1549 . . . . 5  |-  ( A. w A. z ( w  e.  z  ->  A. z  w  e.  z )  ->  A. w ( w  e.  z  <->  w  e.  x ) )
4342a7s 1721 . . . 4  |-  ( A. z A. w ( w  e.  z  ->  A. z  w  e.  z )  ->  A. w ( w  e.  z  <->  w  e.  x ) )
4443a5i 1770 . . 3  |-  ( A. z A. w ( w  e.  z  ->  A. z  w  e.  z )  ->  A. z A. w
( w  e.  z  <-> 
w  e.  x ) )
4515, 28, 443syl 18 . 2  |-  ( A. x A. w ( w  e.  x  <->  w  e.  z )  ->  A. z A. w ( w  e.  z  <->  w  e.  x
) )
46 axext4 2280 . . 3  |-  ( x  =  z  <->  A. w
( w  e.  x  <->  w  e.  z ) )
4746albii 1556 . 2  |-  ( A. x  x  =  z  <->  A. x A. w ( w  e.  x  <->  w  e.  z ) )
48 axext4 2280 . . 3  |-  ( z  =  x  <->  A. w
( w  e.  z  <-> 
w  e.  x ) )
4948albii 1556 . 2  |-  ( A. z  z  =  x  <->  A. z A. w ( w  e.  z  <->  w  e.  x ) )
5045, 47, 493imtr4i 257 1  |-  ( A. x  x  =  z  ->  A. z  z  =  x )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   A.wal 1530   E.wex 1531    = wceq 1632    e. wcel 1696
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-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
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