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

Proof

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