Theorem axc11next 40161

Description: This theorem shows that, given axext4 2754, we can derive a version of axc11n 2362. However, it is weaker than axc11n 2362 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	⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑧 𝑧 = 𝑥)

Distinct variable group:   𝑥,𝑧

Proof of Theorem axc11next

Dummy variable 𝑤 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax-ext 2750	. . . . . 6 ⊢ (∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → 𝑥 = 𝑧)
2	1	alimi 1774	. . . . 5 ⊢ (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑥 𝑥 = 𝑧)
3		ax-11 2093	. . . . . . 7 ⊢ (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑤∀𝑥(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧))
4		ax9 2063	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧))
5		biimpr 212	. . . . . . . . . . 11 ⊢ ((𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥))
6	5	alimi 1774	. . . . . . . . . 10 ⊢ (∀𝑥(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑥(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥))
7		stdpc5v 1897	. . . . . . . . . 10 ⊢ (∀𝑥(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → (𝑤 ∈ 𝑧 → ∀𝑥 𝑤 ∈ 𝑥))
8	6, 7	syl 17	. . . . . . . . 9 ⊢ (∀𝑥(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑧 → ∀𝑥 𝑤 ∈ 𝑥))
9	4, 8	syl9 77	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (∀𝑥(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥)))
10	9	alimdv 1875	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (∀𝑤∀𝑥(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥)))
11	3, 10	syl5 34	. . . . . 6 ⊢ (𝑥 = 𝑧 → (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥)))
12	11	sps 2113	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑧 → (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥)))
13	2, 12	mpcom 38	. . . 4 ⊢ (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥))
14	13	axc4i 2262	. . 3 ⊢ (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑥∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥))
15		nfa1 2088	. . . . . . . 8 ⊢ Ⅎ𝑥∀𝑥 𝑤 ∈ 𝑥
16	15	19.23 2141	. . . . . . 7 ⊢ (∀𝑥(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) ↔ (∃𝑥 𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥))
17		19.8a 2109	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝑧 → ∃𝑧 𝑤 ∈ 𝑧)
18		elequ2 2064	. . . . . . . . . 10 ⊢ (𝑧 = 𝑥 → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
19	18	cbvexvw 1994	. . . . . . . . 9 ⊢ (∃𝑧 𝑤 ∈ 𝑧 ↔ ∃𝑥 𝑤 ∈ 𝑥)
20	17, 19	sylib 210	. . . . . . . 8 ⊢ (𝑤 ∈ 𝑧 → ∃𝑥 𝑤 ∈ 𝑥)
21	4	cbvalivw 1964	. . . . . . . 8 ⊢ (∀𝑥 𝑤 ∈ 𝑥 → ∀𝑧 𝑤 ∈ 𝑧)
22	20, 21	imim12i 62	. . . . . . 7 ⊢ ((∃𝑥 𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) → (𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧))
23	16, 22	sylbi 209	. . . . . 6 ⊢ (∀𝑥(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) → (𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧))
24	23	alimi 1774	. . . . 5 ⊢ (∀𝑤∀𝑥(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) → ∀𝑤(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧))
25	24	alcoms 2094	. . . 4 ⊢ (∀𝑥∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) → ∀𝑤(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧))
26	25	alrimiv 1886	. . 3 ⊢ (∀𝑥∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) → ∀𝑧∀𝑤(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧))
27		nfa1 2088	. . . . . . . 8 ⊢ Ⅎ𝑧∀𝑧 𝑤 ∈ 𝑧
28	27	19.23 2141	. . . . . . 7 ⊢ (∀𝑧(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) ↔ (∃𝑧 𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧))
29		ax9 2063	. . . . . . . . . 10 ⊢ (𝑧 = 𝑥 → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥))
30	29	spimvw 1954	. . . . . . . . 9 ⊢ (∀𝑧 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥)
31	17, 30	imim12i 62	. . . . . . . 8 ⊢ ((∃𝑧 𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥))
32		19.8a 2109	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑥 → ∃𝑥 𝑤 ∈ 𝑥)
33		elequ2 2064	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧))
34	33	cbvexvw 1994	. . . . . . . . . 10 ⊢ (∃𝑥 𝑤 ∈ 𝑥 ↔ ∃𝑧 𝑤 ∈ 𝑧)
35	32, 34	sylib 210	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝑥 → ∃𝑧 𝑤 ∈ 𝑧)
36		sp 2111	. . . . . . . . 9 ⊢ (∀𝑧 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑧)
37	35, 36	imim12i 62	. . . . . . . 8 ⊢ ((∃𝑧 𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧))
38	31, 37	impbid 204	. . . . . . 7 ⊢ ((∃𝑧 𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
39	28, 38	sylbi 209	. . . . . 6 ⊢ (∀𝑧(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
40	39	alimi 1774	. . . . 5 ⊢ (∀𝑤∀𝑧(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
41	40	alcoms 2094	. . . 4 ⊢ (∀𝑧∀𝑤(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
42	41	axc4i 2262	. . 3 ⊢ (∀𝑧∀𝑤(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → ∀𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
43	14, 26, 42	3syl 18	. 2 ⊢ (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
44		axext4 2754	. . 3 ⊢ (𝑥 = 𝑧 ↔ ∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧))
45	44	albii 1782	. 2 ⊢ (∀𝑥 𝑥 = 𝑧 ↔ ∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧))
46		axext4 2754	. . 3 ⊢ (𝑧 = 𝑥 ↔ ∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
47	46	albii 1782	. 2 ⊢ (∀𝑧 𝑧 = 𝑥 ↔ ∀𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
48	43, 45, 47	3imtr4i 284	1 ⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑧 𝑧 = 𝑥)

Syntax hints:   → wi 4   ↔ wb 198  ∀wal 1505   = wceq 1507  ∃wex 1742   ∈ wcel 2050

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-ext 2750

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-ex 1743  df-nf 1747

This theorem is referenced by: (None)