Theorem axc11next 45484

Description: This theorem shows that, given axextb 2735, we can derive a version of axc11n 2455. However, it is weaker than axc11n 2455 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 2732	. . . . . 6 ⊢ (∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → 𝑥 = 𝑧)
2	1	alimi 1843	. . . . 5 ⊢ (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑥 𝑥 = 𝑧)
3		ax-11 2193	. . . . . . 7 ⊢ (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑤∀𝑥(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧))
4		ax9 2158	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧))
5		biimpr 223	. . . . . . . . . . 11 ⊢ ((𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥))
6	5	alimi 1843	. . . . . . . . . 10 ⊢ (∀𝑥(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑥(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥))
7		stdpc5v 1970	. . . . . . . . . 10 ⊢ (∀𝑥(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → (𝑤 ∈ 𝑧 → ∀𝑥 𝑤 ∈ 𝑥))
8	6, 7	syl 18	. . . . . . . . 9 ⊢ (∀𝑥(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑧 → ∀𝑥 𝑤 ∈ 𝑥))
9	4, 8	syl9 78	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (∀𝑥(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥)))
10	9	alimdv 1948	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (∀𝑤∀𝑥(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥)))
11	3, 10	syl5 35	. . . . . 6 ⊢ (𝑥 = 𝑧 → (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥)))
12	11	sps 2221	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑧 → (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥)))
13	2, 12	mpcom 39	. . . 4 ⊢ (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥))
14	13	axc4i 2352	. . 3 ⊢ (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑥∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥))
15		nfa1 2187	. . . . . . . 8 ⊢ Ⅎ𝑥∀𝑥 𝑤 ∈ 𝑥
16	15	19.23 2247	. . . . . . 7 ⊢ (∀𝑥(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) ↔ (∃𝑥 𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥))
17		19.8a 2217	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝑧 → ∃𝑧 𝑤 ∈ 𝑧)
18		elequ2 2159	. . . . . . . . . 10 ⊢ (𝑧 = 𝑥 → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
19	18	cbvexvw 2069	. . . . . . . . 9 ⊢ (∃𝑧 𝑤 ∈ 𝑧 ↔ ∃𝑥 𝑤 ∈ 𝑥)
20	17, 19	sylib 221	. . . . . . . 8 ⊢ (𝑤 ∈ 𝑧 → ∃𝑥 𝑤 ∈ 𝑥)
21	4	cbvalivw 2039	. . . . . . . 8 ⊢ (∀𝑥 𝑤 ∈ 𝑥 → ∀𝑧 𝑤 ∈ 𝑧)
22	20, 21	imim12i 63	. . . . . . 7 ⊢ ((∃𝑥 𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) → (𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧))
23	16, 22	sylbi 220	. . . . . 6 ⊢ (∀𝑥(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) → (𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧))
24	23	alimi 1843	. . . . 5 ⊢ (∀𝑤∀𝑥(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) → ∀𝑤(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧))
25	24	alcoms 2194	. . . 4 ⊢ (∀𝑥∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) → ∀𝑤(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧))
26	25	alrimiv 1959	. . 3 ⊢ (∀𝑥∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) → ∀𝑧∀𝑤(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧))
27		nfa1 2187	. . . . . . . 8 ⊢ Ⅎ𝑧∀𝑧 𝑤 ∈ 𝑧
28	27	19.23 2247	. . . . . . 7 ⊢ (∀𝑧(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) ↔ (∃𝑧 𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧))
29		ax9 2158	. . . . . . . . . 10 ⊢ (𝑧 = 𝑥 → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥))
30	29	spimvw 2018	. . . . . . . . 9 ⊢ (∀𝑧 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥)
31	17, 30	imim12i 63	. . . . . . . 8 ⊢ ((∃𝑧 𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥))
32		19.8a 2217	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑥 → ∃𝑥 𝑤 ∈ 𝑥)
33		elequ2 2159	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧))
34	33	cbvexvw 2069	. . . . . . . . . 10 ⊢ (∃𝑥 𝑤 ∈ 𝑥 ↔ ∃𝑧 𝑤 ∈ 𝑧)
35	32, 34	sylib 221	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝑥 → ∃𝑧 𝑤 ∈ 𝑧)
36		sp 2219	. . . . . . . . 9 ⊢ (∀𝑧 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑧)
37	35, 36	imim12i 63	. . . . . . . 8 ⊢ ((∃𝑧 𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧))
38	31, 37	impbid 215	. . . . . . 7 ⊢ ((∃𝑧 𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
39	28, 38	sylbi 220	. . . . . 6 ⊢ (∀𝑧(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
40	39	alimi 1843	. . . . 5 ⊢ (∀𝑤∀𝑧(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
41	40	alcoms 2194	. . . 4 ⊢ (∀𝑧∀𝑤(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
42	41	axc4i 2352	. . 3 ⊢ (∀𝑧∀𝑤(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → ∀𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
43	14, 26, 42	3syl 19	. 2 ⊢ (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
44		axextb 2735	. . 3 ⊢ (𝑥 = 𝑧 ↔ ∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧))
45	44	albii 1851	. 2 ⊢ (∀𝑥 𝑥 = 𝑧 ↔ ∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧))
46		axextb 2735	. . 3 ⊢ (𝑧 = 𝑥 ↔ ∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
47	46	albii 1851	. 2 ⊢ (∀𝑧 𝑧 = 𝑥 ↔ ∀𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
48	43, 45, 47	3imtr4i 295	1 ⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑧 𝑧 = 𝑥)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209  ∀wal 1567   = wceq 1569  ∃wex 1811   ∈ wcel 2144

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732

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

This theorem is used by: (None)