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

Theorem ax10ext 27574
Description: This theorem shows that, given axext4 2419, we can derive a version of ax10 2025. However, it is weaker than ax10 2025 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 2416 . . . . . 6  |-  ( A. w ( w  e.  x  <->  w  e.  z
)  ->  x  =  z )
21alimi 1568 . . . . 5  |-  ( A. x A. w ( w  e.  x  <->  w  e.  z )  ->  A. x  x  =  z )
3 ax-7 1749 . . . . . . 7  |-  ( A. x A. w ( w  e.  x  <->  w  e.  z )  ->  A. w A. x ( w  e.  x  <->  w  e.  z
) )
4 ax-14 1729 . . . . . . . . 9  |-  ( x  =  z  ->  (
w  e.  x  ->  w  e.  z )
)
5 bi2 190 . . . . . . . . . . 11  |-  ( ( w  e.  x  <->  w  e.  z )  ->  (
w  e.  z  ->  w  e.  x )
)
65alimi 1568 . . . . . . . . . 10  |-  ( A. x ( w  e.  x  <->  w  e.  z
)  ->  A. x
( w  e.  z  ->  w  e.  x
) )
7 nfv 1629 . . . . . . . . . . 11  |-  F/ x  w  e.  z
87stdpc5 1816 . . . . . . . . . 10  |-  ( A. x ( w  e.  z  ->  w  e.  x )  ->  (
w  e.  z  ->  A. x  w  e.  x ) )
96, 8syl 16 . . . . . . . . 9  |-  ( A. x ( w  e.  x  <->  w  e.  z
)  ->  ( w  e.  z  ->  A. x  w  e.  x )
)
104, 9syl9 68 . . . . . . . 8  |-  ( x  =  z  ->  ( A. x ( w  e.  x  <->  w  e.  z
)  ->  ( w  e.  x  ->  A. x  w  e.  x )
) )
1110alimdv 1631 . . . . . . 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 30 . . . . . 6  |-  ( x  =  z  ->  ( A. x A. w ( w  e.  x  <->  w  e.  z )  ->  A. w
( w  e.  x  ->  A. x  w  e.  x ) ) )
1312sps 1770 . . . . 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 34 . . . 4  |-  ( A. x A. w ( w  e.  x  <->  w  e.  z )  ->  A. w
( w  e.  x  ->  A. x  w  e.  x ) )
1514a5i 1807 . . 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 1806 . . . . . . . 8  |-  F/ x A. x  w  e.  x
171619.23 1819 . . . . . . 7  |-  ( A. x ( w  e.  x  ->  A. x  w  e.  x )  <->  ( E. x  w  e.  x  ->  A. x  w  e.  x )
)
18 19.8a 1762 . . . . . . . . 9  |-  ( w  e.  z  ->  E. z  w  e.  z )
19 elequ2 1730 . . . . . . . . . 10  |-  ( z  =  x  ->  (
w  e.  z  <->  w  e.  x ) )
2019cbvexv 1985 . . . . . . . . 9  |-  ( E. z  w  e.  z  <->  E. x  w  e.  x )
2118, 20sylib 189 . . . . . . . 8  |-  ( w  e.  z  ->  E. x  w  e.  x )
22 nfv 1629 . . . . . . . . 9  |-  F/ z  w  e.  x
2322, 7, 4cbv3 1971 . . . . . . . 8  |-  ( A. x  w  e.  x  ->  A. z  w  e.  z )
2421, 23imim12i 55 . . . . . . 7  |-  ( ( E. x  w  e.  x  ->  A. x  w  e.  x )  ->  ( w  e.  z  ->  A. z  w  e.  z ) )
2517, 24sylbi 188 . . . . . 6  |-  ( A. x ( w  e.  x  ->  A. x  w  e.  x )  ->  ( w  e.  z  ->  A. z  w  e.  z ) )
2625alimi 1568 . . . . 5  |-  ( A. w A. x ( w  e.  x  ->  A. x  w  e.  x )  ->  A. w ( w  e.  z  ->  A. z  w  e.  z )
)
2726a7s 1750 . . . 4  |-  ( A. x A. w ( w  e.  x  ->  A. x  w  e.  x )  ->  A. w ( w  e.  z  ->  A. z  w  e.  z )
)
2827alrimiv 1641 . . 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 1806 . . . . . . . 8  |-  F/ z A. z  w  e.  z
302919.23 1819 . . . . . . 7  |-  ( A. z ( w  e.  z  ->  A. z  w  e.  z )  <->  ( E. z  w  e.  z  ->  A. z  w  e.  z )
)
31 ax-14 1729 . . . . . . . . . 10  |-  ( z  =  x  ->  (
w  e.  z  ->  w  e.  x )
)
3231spimv 1963 . . . . . . . . 9  |-  ( A. z  w  e.  z  ->  w  e.  x )
3318, 32imim12i 55 . . . . . . . 8  |-  ( ( E. z  w  e.  z  ->  A. z  w  e.  z )  ->  ( w  e.  z  ->  w  e.  x
) )
34 19.8a 1762 . . . . . . . . . 10  |-  ( w  e.  x  ->  E. x  w  e.  x )
35 elequ2 1730 . . . . . . . . . . 11  |-  ( x  =  z  ->  (
w  e.  x  <->  w  e.  z ) )
3635cbvexv 1985 . . . . . . . . . 10  |-  ( E. x  w  e.  x  <->  E. z  w  e.  z )
3734, 36sylib 189 . . . . . . . . 9  |-  ( w  e.  x  ->  E. z  w  e.  z )
38 sp 1763 . . . . . . . . 9  |-  ( A. z  w  e.  z  ->  w  e.  z )
3937, 38imim12i 55 . . . . . . . 8  |-  ( ( E. z  w  e.  z  ->  A. z  w  e.  z )  ->  ( w  e.  x  ->  w  e.  z ) )
4033, 39impbid 184 . . . . . . 7  |-  ( ( E. z  w  e.  z  ->  A. z  w  e.  z )  ->  ( w  e.  z  <-> 
w  e.  x ) )
4130, 40sylbi 188 . . . . . 6  |-  ( A. z ( w  e.  z  ->  A. z  w  e.  z )  ->  ( w  e.  z  <-> 
w  e.  x ) )
4241alimi 1568 . . . . 5  |-  ( A. w A. z ( w  e.  z  ->  A. z  w  e.  z )  ->  A. w ( w  e.  z  <->  w  e.  x ) )
4342a7s 1750 . . . 4  |-  ( A. z A. w ( w  e.  z  ->  A. z  w  e.  z )  ->  A. w ( w  e.  z  <->  w  e.  x ) )
4443a5i 1807 . . 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 19 . 2  |-  ( A. x A. w ( w  e.  x  <->  w  e.  z )  ->  A. z A. w ( w  e.  z  <->  w  e.  x
) )
46 axext4 2419 . . 3  |-  ( x  =  z  <->  A. w
( w  e.  x  <->  w  e.  z ) )
4746albii 1575 . 2  |-  ( A. x  x  =  z  <->  A. x A. w ( w  e.  x  <->  w  e.  z ) )
48 axext4 2419 . . 3  |-  ( z  =  x  <->  A. w
( w  e.  z  <-> 
w  e.  x ) )
4948albii 1575 . 2  |-  ( A. z  z  =  x  <->  A. z A. w ( w  e.  z  <->  w  e.  x ) )
5045, 47, 493imtr4i 258 1  |-  ( A. x  x  =  z  ->  A. z  z  =  x )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   A.wal 1549   E.wex 1550    = wceq 1652    e. wcel 1725
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554
  Copyright terms: Public domain W3C validator