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 ⊢ ∀ x x = z → ∀ z z = x

Proof

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