Theorem axc11next 45349

Description: This theorem shows that, given axextb 2736, we can derive a version of axc11n 2456. However, it is weaker than axc11n 2456 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 2733	. . . . . 6 ⊢ (∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → 𝑥 = 𝑧)
2	1	alimi 1844	. . . . 5 ⊢ (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑥 𝑥 = 𝑧)
3		ax-11 2194	. . . . . . 7 ⊢ (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑤∀𝑥(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧))
4		ax9 2159	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧))
5		biimpr 223	. . . . . . . . . . 11 ⊢ ((𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥))
6	5	alimi 1844	. . . . . . . . . 10 ⊢ (∀𝑥(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑥(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥))
7		stdpc5v 1971	. . . . . . . . . 10 ⊢ (∀𝑥(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → (𝑤 ∈ 𝑧 → ∀𝑥 𝑤 ∈ 𝑥))
8	6, 7	syl 18	. . . . . . . . 9 ⊢ (∀𝑥(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑧 → ∀𝑥 𝑤 ∈ 𝑥))
9	4, 8	syl9 78	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (∀𝑥(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥)))
10	9	alimdv 1949	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (∀𝑤∀𝑥(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥)))
11	3, 10	syl5 35	. . . . . 6 ⊢ (𝑥 = 𝑧 → (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥)))
12	11	sps 2222	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑧 → (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥)))
13	2, 12	mpcom 39	. . . 4 ⊢ (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥))
14	13	axc4i 2353	. . 3 ⊢ (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑥∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥))
15		nfa1 2188	. . . . . . . 8 ⊢ Ⅎ𝑥∀𝑥 𝑤 ∈ 𝑥
16	15	19.23 2248	. . . . . . 7 ⊢ (∀𝑥(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) ↔ (∃𝑥 𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥))
17		19.8a 2218	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝑧 → ∃𝑧 𝑤 ∈ 𝑧)
18		elequ2 2160	. . . . . . . . . 10 ⊢ (𝑧 = 𝑥 → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
19	18	cbvexvw 2070	. . . . . . . . 9 ⊢ (∃𝑧 𝑤 ∈ 𝑧 ↔ ∃𝑥 𝑤 ∈ 𝑥)
20	17, 19	sylib 221	. . . . . . . 8 ⊢ (𝑤 ∈ 𝑧 → ∃𝑥 𝑤 ∈ 𝑥)
21	4	cbvalivw 2040	. . . . . . . 8 ⊢ (∀𝑥 𝑤 ∈ 𝑥 → ∀𝑧 𝑤 ∈ 𝑧)
22	20, 21	imim12i 63	. . . . . . 7 ⊢ ((∃𝑥 𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) → (𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧))
23	16, 22	sylbi 220	. . . . . 6 ⊢ (∀𝑥(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) → (𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧))
24	23	alimi 1844	. . . . 5 ⊢ (∀𝑤∀𝑥(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) → ∀𝑤(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧))
25	24	alcoms 2195	. . . 4 ⊢ (∀𝑥∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) → ∀𝑤(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧))
26	25	alrimiv 1960	. . 3 ⊢ (∀𝑥∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) → ∀𝑧∀𝑤(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧))
27		nfa1 2188	. . . . . . . 8 ⊢ Ⅎ𝑧∀𝑧 𝑤 ∈ 𝑧
28	27	19.23 2248	. . . . . . 7 ⊢ (∀𝑧(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) ↔ (∃𝑧 𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧))
29		ax9 2159	. . . . . . . . . 10 ⊢ (𝑧 = 𝑥 → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥))
30	29	spimvw 2019	. . . . . . . . 9 ⊢ (∀𝑧 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥)
31	17, 30	imim12i 63	. . . . . . . 8 ⊢ ((∃𝑧 𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥))
32		19.8a 2218	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑥 → ∃𝑥 𝑤 ∈ 𝑥)
33		elequ2 2160	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧))
34	33	cbvexvw 2070	. . . . . . . . . 10 ⊢ (∃𝑥 𝑤 ∈ 𝑥 ↔ ∃𝑧 𝑤 ∈ 𝑧)
35	32, 34	sylib 221	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝑥 → ∃𝑧 𝑤 ∈ 𝑧)
36		sp 2220	. . . . . . . . 9 ⊢ (∀𝑧 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑧)
37	35, 36	imim12i 63	. . . . . . . 8 ⊢ ((∃𝑧 𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧))
38	31, 37	impbid 215	. . . . . . 7 ⊢ ((∃𝑧 𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
39	28, 38	sylbi 220	. . . . . 6 ⊢ (∀𝑧(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
40	39	alimi 1844	. . . . 5 ⊢ (∀𝑤∀𝑧(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
41	40	alcoms 2195	. . . 4 ⊢ (∀𝑧∀𝑤(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
42	41	axc4i 2353	. . 3 ⊢ (∀𝑧∀𝑤(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → ∀𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
43	14, 26, 42	3syl 19	. 2 ⊢ (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
44		axextb 2736	. . 3 ⊢ (𝑥 = 𝑧 ↔ ∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧))
45	44	albii 1852	. 2 ⊢ (∀𝑥 𝑥 = 𝑧 ↔ ∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧))
46		axextb 2736	. . 3 ⊢ (𝑧 = 𝑥 ↔ ∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
47	46	albii 1852	. 2 ⊢ (∀𝑧 𝑧 = 𝑥 ↔ ∀𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
48	43, 45, 47	3imtr4i 295	1 ⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑧 𝑧 = 𝑥)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-ex 1813  df-nf 1817

This theorem is used by: (None)