Theorem axc11next 44425

Description: This theorem shows that, given axextb 2711, we can derive a version of axc11n 2431. However, it is weaker than axc11n 2431 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 2708	. . . . . 6 ⊢ (∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → 𝑥 = 𝑧)
2	1	alimi 1811	. . . . 5 ⊢ (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑥 𝑥 = 𝑧)
3		ax-11 2157	. . . . . . 7 ⊢ (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑤∀𝑥(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧))
4		ax9 2122	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧))
5		biimpr 220	. . . . . . . . . . 11 ⊢ ((𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥))
6	5	alimi 1811	. . . . . . . . . 10 ⊢ (∀𝑥(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑥(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥))
7		stdpc5v 1938	. . . . . . . . . 10 ⊢ (∀𝑥(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → (𝑤 ∈ 𝑧 → ∀𝑥 𝑤 ∈ 𝑥))
8	6, 7	syl 17	. . . . . . . . 9 ⊢ (∀𝑥(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑧 → ∀𝑥 𝑤 ∈ 𝑥))
9	4, 8	syl9 77	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (∀𝑥(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥)))
10	9	alimdv 1916	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (∀𝑤∀𝑥(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥)))
11	3, 10	syl5 34	. . . . . 6 ⊢ (𝑥 = 𝑧 → (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥)))
12	11	sps 2185	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑧 → (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥)))
13	2, 12	mpcom 38	. . . 4 ⊢ (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥))
14	13	axc4i 2322	. . 3 ⊢ (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑥∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥))
15		nfa1 2151	. . . . . . . 8 ⊢ Ⅎ𝑥∀𝑥 𝑤 ∈ 𝑥
16	15	19.23 2211	. . . . . . 7 ⊢ (∀𝑥(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) ↔ (∃𝑥 𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥))
17		19.8a 2181	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝑧 → ∃𝑧 𝑤 ∈ 𝑧)
18		elequ2 2123	. . . . . . . . . 10 ⊢ (𝑧 = 𝑥 → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
19	18	cbvexvw 2036	. . . . . . . . 9 ⊢ (∃𝑧 𝑤 ∈ 𝑧 ↔ ∃𝑥 𝑤 ∈ 𝑥)
20	17, 19	sylib 218	. . . . . . . 8 ⊢ (𝑤 ∈ 𝑧 → ∃𝑥 𝑤 ∈ 𝑥)
21	4	cbvalivw 2006	. . . . . . . 8 ⊢ (∀𝑥 𝑤 ∈ 𝑥 → ∀𝑧 𝑤 ∈ 𝑧)
22	20, 21	imim12i 62	. . . . . . 7 ⊢ ((∃𝑥 𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) → (𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧))
23	16, 22	sylbi 217	. . . . . 6 ⊢ (∀𝑥(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) → (𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧))
24	23	alimi 1811	. . . . 5 ⊢ (∀𝑤∀𝑥(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) → ∀𝑤(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧))
25	24	alcoms 2158	. . . 4 ⊢ (∀𝑥∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) → ∀𝑤(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧))
26	25	alrimiv 1927	. . 3 ⊢ (∀𝑥∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) → ∀𝑧∀𝑤(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧))
27		nfa1 2151	. . . . . . . 8 ⊢ Ⅎ𝑧∀𝑧 𝑤 ∈ 𝑧
28	27	19.23 2211	. . . . . . 7 ⊢ (∀𝑧(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) ↔ (∃𝑧 𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧))
29		ax9 2122	. . . . . . . . . 10 ⊢ (𝑧 = 𝑥 → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥))
30	29	spimvw 1995	. . . . . . . . 9 ⊢ (∀𝑧 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥)
31	17, 30	imim12i 62	. . . . . . . 8 ⊢ ((∃𝑧 𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥))
32		19.8a 2181	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑥 → ∃𝑥 𝑤 ∈ 𝑥)
33		elequ2 2123	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧))
34	33	cbvexvw 2036	. . . . . . . . . 10 ⊢ (∃𝑥 𝑤 ∈ 𝑥 ↔ ∃𝑧 𝑤 ∈ 𝑧)
35	32, 34	sylib 218	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝑥 → ∃𝑧 𝑤 ∈ 𝑧)
36		sp 2183	. . . . . . . . 9 ⊢ (∀𝑧 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑧)
37	35, 36	imim12i 62	. . . . . . . 8 ⊢ ((∃𝑧 𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧))
38	31, 37	impbid 212	. . . . . . 7 ⊢ ((∃𝑧 𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
39	28, 38	sylbi 217	. . . . . 6 ⊢ (∀𝑧(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
40	39	alimi 1811	. . . . 5 ⊢ (∀𝑤∀𝑧(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
41	40	alcoms 2158	. . . 4 ⊢ (∀𝑧∀𝑤(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
42	41	axc4i 2322	. . 3 ⊢ (∀𝑧∀𝑤(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → ∀𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
43	14, 26, 42	3syl 18	. 2 ⊢ (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
44		axextb 2711	. . 3 ⊢ (𝑥 = 𝑧 ↔ ∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧))
45	44	albii 1819	. 2 ⊢ (∀𝑥 𝑥 = 𝑧 ↔ ∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧))
46		axextb 2711	. . 3 ⊢ (𝑧 = 𝑥 ↔ ∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
47	46	albii 1819	. 2 ⊢ (∀𝑧 𝑧 = 𝑥 ↔ ∀𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
48	43, 45, 47	3imtr4i 292	1 ⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑧 𝑧 = 𝑥)

Syntax hints:   → wi 4   ↔ wb 206  ∀wal 1538   = wceq 1540  ∃wex 1779   ∈ wcel 2108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-nf 1784

This theorem is referenced by: (None)