Metamath Proof Explorer

Theorem axc11next

Description: This theorem shows that, given axextb , we can derive a version of axc11n . However, it is weaker than axc11n because it has a distinct variable requirement. (Contributed by Andrew Salmon, 16-Jul-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion axc11next 
|- ( A. x x = z -> A. z z = x )

Proof

Step Hyp Ref Expression
1 ax-ext 
 |-  ( A. w ( w e. x <-> w e. z ) -> x = z )
2 1 alimi 
 |-  ( A. x A. w ( w e. x <-> w e. z ) -> A. x x = z )
3 ax-11 
 |-  ( A. x A. w ( w e. x <-> w e. z ) -> A. w A. x ( w e. x <-> w e. z ) )
4 ax9 
 |-  ( x = z -> ( w e. x -> w e. z ) )
5 biimpr 
 |-  ( ( w e. x <-> w e. z ) -> ( w e. z -> w e. x ) )
6 5 alimi 
 |-  ( A. x ( w e. x <-> w e. z ) -> A. x ( w e. z -> w e. x ) )
7 stdpc5v 
 |-  ( A. x ( w e. z -> w e. x ) -> ( w e. z -> A. x w e. x ) )
8 6 7 syl 
 |-  ( A. x ( w e. x <-> w e. z ) -> ( w e. z -> A. x w e. x ) )
9 4 8 syl9 
 |-  ( x = z -> ( A. x ( w e. x <-> w e. z ) -> ( w e. x -> A. x w e. x ) ) )
10 9 alimdv 
 |-  ( x = z -> ( A. w A. x ( w e. x <-> w e. z ) -> A. w ( w e. x -> A. x w e. x ) ) )
11 3 10 syl5 
 |-  ( x = z -> ( A. x A. w ( w e. x <-> w e. z ) -> A. w ( w e. x -> A. x w e. x ) ) )
12 11 sps 
 |-  ( A. x x = z -> ( A. x A. w ( w e. x <-> w e. z ) -> A. w ( w e. x -> A. x w e. x ) ) )
13 2 12 mpcom 
 |-  ( A. x A. w ( w e. x <-> w e. z ) -> A. w ( w e. x -> A. x w e. x ) )
14 13 axc4i 
 |-  ( A. x A. w ( w e. x <-> w e. z ) -> A. x A. w ( w e. x -> A. x w e. x ) )
15 nfa1 
 |-  F/ x A. x w e. x
16 15 19.23 
 |-  ( A. x ( w e. x -> A. x w e. x ) <-> ( E. x w e. x -> A. x w e. x ) )
17 19.8a 
 |-  ( w e. z -> E. z w e. z )
18 elequ2 
 |-  ( z = x -> ( w e. z <-> w e. x ) )
19 18 cbvexvw 
 |-  ( E. z w e. z <-> E. x w e. x )
20 17 19 sylib 
 |-  ( w e. z -> E. x w e. x )
21 4 cbvalivw 
 |-  ( A. x w e. x -> A. z w e. z )
22 20 21 imim12i 
 |-  ( ( E. x w e. x -> A. x w e. x ) -> ( w e. z -> A. z w e. z ) )
23 16 22 sylbi 
 |-  ( A. x ( w e. x -> A. x w e. x ) -> ( w e. z -> A. z w e. z ) )
24 23 alimi 
 |-  ( A. w A. x ( w e. x -> A. x w e. x ) -> A. w ( w e. z -> A. z w e. z ) )
25 24 alcoms 
 |-  ( A. x A. w ( w e. x -> A. x w e. x ) -> A. w ( w e. z -> A. z w e. z ) )
26 25 alrimiv 
 |-  ( A. x A. w ( w e. x -> A. x w e. x ) -> A. z A. w ( w e. z -> A. z w e. z ) )
27 nfa1 
 |-  F/ z A. z w e. z
28 27 19.23 
 |-  ( A. z ( w e. z -> A. z w e. z ) <-> ( E. z w e. z -> A. z w e. z ) )
29 ax9 
 |-  ( z = x -> ( w e. z -> w e. x ) )
30 29 spimvw 
 |-  ( A. z w e. z -> w e. x )
31 17 30 imim12i 
 |-  ( ( E. z w e. z -> A. z w e. z ) -> ( w e. z -> w e. x ) )
32 19.8a 
 |-  ( w e. x -> E. x w e. x )
33 elequ2 
 |-  ( x = z -> ( w e. x <-> w e. z ) )
34 33 cbvexvw 
 |-  ( E. x w e. x <-> E. z w e. z )
35 32 34 sylib 
 |-  ( w e. x -> E. z w e. z )
36 sp 
 |-  ( A. z w e. z -> w e. z )
37 35 36 imim12i 
 |-  ( ( E. z w e. z -> A. z w e. z ) -> ( w e. x -> w e. z ) )
38 31 37 impbid 
 |-  ( ( E. z w e. z -> A. z w e. z ) -> ( w e. z <-> w e. x ) )
39 28 38 sylbi 
 |-  ( A. z ( w e. z -> A. z w e. z ) -> ( w e. z <-> w e. x ) )
40 39 alimi 
 |-  ( A. w A. z ( w e. z -> A. z w e. z ) -> A. w ( w e. z <-> w e. x ) )
41 40 alcoms 
 |-  ( A. z A. w ( w e. z -> A. z w e. z ) -> A. w ( w e. z <-> w e. x ) )
42 41 axc4i 
 |-  ( A. z A. w ( w e. z -> A. z w e. z ) -> A. z A. w ( w e. z <-> w e. x ) )
43 14 26 42 3syl 
 |-  ( A. x A. w ( w e. x <-> w e. z ) -> A. z A. w ( w e. z <-> w e. x ) )
44 axextb 
 |-  ( x = z <-> A. w ( w e. x <-> w e. z ) )
45 44 albii 
 |-  ( A. x x = z <-> A. x A. w ( w e. x <-> w e. z ) )
46 axextb 
 |-  ( z = x <-> A. w ( w e. z <-> w e. x ) )
47 46 albii 
 |-  ( A. z z = x <-> A. z A. w ( w e. z <-> w e. x ) )
48 43 45 47 3imtr4i 
 |-  ( A. x x = z -> A. z z = x )