Theorem axc11next 45099

Description: This theorem shows that, given axextb 2738, we can derive a version of axc11n 2458. However, it is weaker than axc11n 2458 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 2735	. . . . . 6 ⊢ (∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → 𝑥 = 𝑧)
2	1	alimi 1841	. . . . 5 ⊢ (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑥 𝑥 = 𝑧)
3		ax-11 2192	. . . . . . 7 ⊢ (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑤∀𝑥(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧))
4		ax9 2157	. . . . . . . . 9 ⊢ (𝑥 = 𝑧 → (𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧))
5		biimpr 223	. . . . . . . . . . 11 ⊢ ((𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥))
6	5	alimi 1841	. . . . . . . . . 10 ⊢ (∀𝑥(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑥(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥))
7		stdpc5v 1968	. . . . . . . . . 10 ⊢ (∀𝑥(𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → (𝑤 ∈ 𝑧 → ∀𝑥 𝑤 ∈ 𝑥))
8	6, 7	syl 18	. . . . . . . . 9 ⊢ (∀𝑥(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑧 → ∀𝑥 𝑤 ∈ 𝑥))
9	4, 8	syl9 78	. . . . . . . 8 ⊢ (𝑥 = 𝑧 → (∀𝑥(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥)))
10	9	alimdv 1946	. . . . . . 7 ⊢ (𝑥 = 𝑧 → (∀𝑤∀𝑥(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥)))
11	3, 10	syl5 35	. . . . . 6 ⊢ (𝑥 = 𝑧 → (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥)))
12	11	sps 2221	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑧 → (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥)))
13	2, 12	mpcom 39	. . . 4 ⊢ (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥))
14	13	axc4i 2355	. . 3 ⊢ (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑥∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥))
15		nfa1 2186	. . . . . . . 8 ⊢ Ⅎ𝑥∀𝑥 𝑤 ∈ 𝑥
16	15	19.23 2247	. . . . . . 7 ⊢ (∀𝑥(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) ↔ (∃𝑥 𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥))
17		19.8a 2217	. . . . . . . . 9 ⊢ (𝑤 ∈ 𝑧 → ∃𝑧 𝑤 ∈ 𝑧)
18		elequ2 2158	. . . . . . . . . 10 ⊢ (𝑧 = 𝑥 → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
19	18	cbvexvw 2067	. . . . . . . . 9 ⊢ (∃𝑧 𝑤 ∈ 𝑧 ↔ ∃𝑥 𝑤 ∈ 𝑥)
20	17, 19	sylib 221	. . . . . . . 8 ⊢ (𝑤 ∈ 𝑧 → ∃𝑥 𝑤 ∈ 𝑥)
21	4	cbvalivw 2037	. . . . . . . 8 ⊢ (∀𝑥 𝑤 ∈ 𝑥 → ∀𝑧 𝑤 ∈ 𝑧)
22	20, 21	imim12i 63	. . . . . . 7 ⊢ ((∃𝑥 𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) → (𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧))
23	16, 22	sylbi 220	. . . . . 6 ⊢ (∀𝑥(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) → (𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧))
24	23	alimi 1841	. . . . 5 ⊢ (∀𝑤∀𝑥(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) → ∀𝑤(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧))
25	24	alcoms 2193	. . . 4 ⊢ (∀𝑥∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) → ∀𝑤(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧))
26	25	alrimiv 1957	. . 3 ⊢ (∀𝑥∀𝑤(𝑤 ∈ 𝑥 → ∀𝑥 𝑤 ∈ 𝑥) → ∀𝑧∀𝑤(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧))
27		nfa1 2186	. . . . . . . 8 ⊢ Ⅎ𝑧∀𝑧 𝑤 ∈ 𝑧
28	27	19.23 2247	. . . . . . 7 ⊢ (∀𝑧(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) ↔ (∃𝑧 𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧))
29		ax9 2157	. . . . . . . . . 10 ⊢ (𝑧 = 𝑥 → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥))
30	29	spimvw 2016	. . . . . . . . 9 ⊢ (∀𝑧 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥)
31	17, 30	imim12i 63	. . . . . . . 8 ⊢ ((∃𝑧 𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥))
32		19.8a 2217	. . . . . . . . . 10 ⊢ (𝑤 ∈ 𝑥 → ∃𝑥 𝑤 ∈ 𝑥)
33		elequ2 2158	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑧 → (𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧))
34	33	cbvexvw 2067	. . . . . . . . . 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 1841	. . . . 5 ⊢ (∀𝑤∀𝑧(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
41	40	alcoms 2193	. . . 4 ⊢ (∀𝑧∀𝑤(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → ∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
42	41	axc4i 2355	. . 3 ⊢ (∀𝑧∀𝑤(𝑤 ∈ 𝑧 → ∀𝑧 𝑤 ∈ 𝑧) → ∀𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
43	14, 26, 42	3syl 19	. 2 ⊢ (∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧) → ∀𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
44		axextb 2738	. . 3 ⊢ (𝑥 = 𝑧 ↔ ∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧))
45	44	albii 1849	. 2 ⊢ (∀𝑥 𝑥 = 𝑧 ↔ ∀𝑥∀𝑤(𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧))
46		axextb 2738	. . 3 ⊢ (𝑧 = 𝑥 ↔ ∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
47	46	albii 1849	. 2 ⊢ (∀𝑧 𝑧 = 𝑥 ↔ ∀𝑧∀𝑤(𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥))
48	43, 45, 47	3imtr4i 295	1 ⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑧 𝑧 = 𝑥)

Syntax hints:   → wi 4   ↔ wb 209  ∀wal 1568   = wceq 1570  ∃wex 1809   ∈ wcel 2143

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-ex 1810  df-nf 1814

This theorem is referenced by: (None)