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

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

Proof of Theorem axc11next
Dummy variable  w is distinct from all other variables.
StepHypRef Expression
1 ax-ext 2445 . . . . . 6  |-  ( A. w ( w  e.  x  <->  w  e.  z
)  ->  x  =  z )
21alimi 1614 . . . . 5  |-  ( A. x A. w ( w  e.  x  <->  w  e.  z )  ->  A. x  x  =  z )
3 ax-11 1791 . . . . . . 7  |-  ( A. x A. w ( w  e.  x  <->  w  e.  z )  ->  A. w A. x ( w  e.  x  <->  w  e.  z
) )
4 ax-9 1771 . . . . . . . . 9  |-  ( x  =  z  ->  (
w  e.  x  ->  w  e.  z )
)
5 bi2 198 . . . . . . . . . . 11  |-  ( ( w  e.  x  <->  w  e.  z )  ->  (
w  e.  z  ->  w  e.  x )
)
65alimi 1614 . . . . . . . . . 10  |-  ( A. x ( w  e.  x  <->  w  e.  z
)  ->  A. x
( w  e.  z  ->  w  e.  x
) )
7 nfv 1683 . . . . . . . . . . 11  |-  F/ x  w  e.  z
87stdpc5 1855 . . . . . . . . . 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 71 . . . . . . . 8  |-  ( x  =  z  ->  ( A. x ( w  e.  x  <->  w  e.  z
)  ->  ( w  e.  x  ->  A. x  w  e.  x )
) )
1110alimdv 1685 . . . . . . 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 32 . . . . . 6  |-  ( x  =  z  ->  ( A. x A. w ( w  e.  x  <->  w  e.  z )  ->  A. w
( w  e.  x  ->  A. x  w  e.  x ) ) )
1312sps 1814 . . . . 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 36 . . . 4  |-  ( A. x A. w ( w  e.  x  <->  w  e.  z )  ->  A. w
( w  e.  x  ->  A. x  w  e.  x ) )
1514axc4i 1846 . . 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 1845 . . . . . . . 8  |-  F/ x A. x  w  e.  x
171619.23 1857 . . . . . . 7  |-  ( A. x ( w  e.  x  ->  A. x  w  e.  x )  <->  ( E. x  w  e.  x  ->  A. x  w  e.  x )
)
18 19.8a 1806 . . . . . . . . 9  |-  ( w  e.  z  ->  E. z  w  e.  z )
19 elequ2 1772 . . . . . . . . . 10  |-  ( z  =  x  ->  (
w  e.  z  <->  w  e.  x ) )
2019cbvexv 1997 . . . . . . . . 9  |-  ( E. z  w  e.  z  <->  E. x  w  e.  x )
2118, 20sylib 196 . . . . . . . 8  |-  ( w  e.  z  ->  E. x  w  e.  x )
22 nfv 1683 . . . . . . . . 9  |-  F/ z  w  e.  x
2322, 7, 4cbv3 1984 . . . . . . . 8  |-  ( A. x  w  e.  x  ->  A. z  w  e.  z )
2421, 23imim12i 57 . . . . . . 7  |-  ( ( E. x  w  e.  x  ->  A. x  w  e.  x )  ->  ( w  e.  z  ->  A. z  w  e.  z ) )
2517, 24sylbi 195 . . . . . 6  |-  ( A. x ( w  e.  x  ->  A. x  w  e.  x )  ->  ( w  e.  z  ->  A. z  w  e.  z ) )
2625alimi 1614 . . . . 5  |-  ( A. w A. x ( w  e.  x  ->  A. x  w  e.  x )  ->  A. w ( w  e.  z  ->  A. z  w  e.  z )
)
2726alcoms 1792 . . . 4  |-  ( A. x A. w ( w  e.  x  ->  A. x  w  e.  x )  ->  A. w ( w  e.  z  ->  A. z  w  e.  z )
)
2827alrimiv 1695 . . 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 1845 . . . . . . . 8  |-  F/ z A. z  w  e.  z
302919.23 1857 . . . . . . 7  |-  ( A. z ( w  e.  z  ->  A. z  w  e.  z )  <->  ( E. z  w  e.  z  ->  A. z  w  e.  z )
)
31 ax-9 1771 . . . . . . . . . 10  |-  ( z  =  x  ->  (
w  e.  z  ->  w  e.  x )
)
3231spimv 1978 . . . . . . . . 9  |-  ( A. z  w  e.  z  ->  w  e.  x )
3318, 32imim12i 57 . . . . . . . 8  |-  ( ( E. z  w  e.  z  ->  A. z  w  e.  z )  ->  ( w  e.  z  ->  w  e.  x
) )
34 19.8a 1806 . . . . . . . . . 10  |-  ( w  e.  x  ->  E. x  w  e.  x )
35 elequ2 1772 . . . . . . . . . . 11  |-  ( x  =  z  ->  (
w  e.  x  <->  w  e.  z ) )
3635cbvexv 1997 . . . . . . . . . 10  |-  ( E. x  w  e.  x  <->  E. z  w  e.  z )
3734, 36sylib 196 . . . . . . . . 9  |-  ( w  e.  x  ->  E. z  w  e.  z )
38 sp 1808 . . . . . . . . 9  |-  ( A. z  w  e.  z  ->  w  e.  z )
3937, 38imim12i 57 . . . . . . . 8  |-  ( ( E. z  w  e.  z  ->  A. z  w  e.  z )  ->  ( w  e.  x  ->  w  e.  z ) )
4033, 39impbid 191 . . . . . . 7  |-  ( ( E. z  w  e.  z  ->  A. z  w  e.  z )  ->  ( w  e.  z  <-> 
w  e.  x ) )
4130, 40sylbi 195 . . . . . 6  |-  ( A. z ( w  e.  z  ->  A. z  w  e.  z )  ->  ( w  e.  z  <-> 
w  e.  x ) )
4241alimi 1614 . . . . 5  |-  ( A. w A. z ( w  e.  z  ->  A. z  w  e.  z )  ->  A. w ( w  e.  z  <->  w  e.  x ) )
4342alcoms 1792 . . . 4  |-  ( A. z A. w ( w  e.  z  ->  A. z  w  e.  z )  ->  A. w ( w  e.  z  <->  w  e.  x ) )
4443axc4i 1846 . . 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 20 . 2  |-  ( A. x A. w ( w  e.  x  <->  w  e.  z )  ->  A. z A. w ( w  e.  z  <->  w  e.  x
) )
46 axext4 2449 . . 3  |-  ( x  =  z  <->  A. w
( w  e.  x  <->  w  e.  z ) )
4746albii 1620 . 2  |-  ( A. x  x  =  z  <->  A. x A. w ( w  e.  x  <->  w  e.  z ) )
48 axext4 2449 . . 3  |-  ( z  =  x  <->  A. w
( w  e.  z  <-> 
w  e.  x ) )
4948albii 1620 . 2  |-  ( A. z  z  =  x  <->  A. z A. w ( w  e.  z  <->  w  e.  x ) )
5045, 47, 493imtr4i 266 1  |-  ( A. x  x  =  z  ->  A. z  z  =  x )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   A.wal 1377    = wceq 1379   E.wex 1596    e. wcel 1767
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1597  df-nf 1600
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator