Theorem axc11next

Description: This theorem shows that, given axextb , we can derive a version of axc11n . However, it is weaker than axc11n because it has a distinct variable requirement. (Contributed by Andrew Salmon, 16-Jul-2011) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	axc11next	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ∀ 𝑧 𝑧 = 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		ax-ext	⊢ ( ∀ 𝑤 ( 𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧 ) → 𝑥 = 𝑧 )
2	1	alimi	⊢ ( ∀ 𝑥 ∀ 𝑤 ( 𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧 ) → ∀ 𝑥 𝑥 = 𝑧 )
3		ax-11	⊢ ( ∀ 𝑥 ∀ 𝑤 ( 𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧 ) → ∀ 𝑤 ∀ 𝑥 ( 𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧 ) )
4		ax9	⊢ ( 𝑥 = 𝑧 → ( 𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧 ) )
5		biimpr	⊢ ( ( 𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) )
6	5	alimi	⊢ ( ∀ 𝑥 ( 𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧 ) → ∀ 𝑥 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) )
7		stdpc5v	⊢ ( ∀ 𝑥 ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) → ( 𝑤 ∈ 𝑧 → ∀ 𝑥 𝑤 ∈ 𝑥 ) )
8	6 7	syl	⊢ ( ∀ 𝑥 ( 𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑧 → ∀ 𝑥 𝑤 ∈ 𝑥 ) )
9	4 8	syl9	⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑥 ( 𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑥 → ∀ 𝑥 𝑤 ∈ 𝑥 ) ) )
10	9	alimdv	⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑤 ∀ 𝑥 ( 𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧 ) → ∀ 𝑤 ( 𝑤 ∈ 𝑥 → ∀ 𝑥 𝑤 ∈ 𝑥 ) ) )
11	3 10	syl5	⊢ ( 𝑥 = 𝑧 → ( ∀ 𝑥 ∀ 𝑤 ( 𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧 ) → ∀ 𝑤 ( 𝑤 ∈ 𝑥 → ∀ 𝑥 𝑤 ∈ 𝑥 ) ) )
12	11	sps	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ( ∀ 𝑥 ∀ 𝑤 ( 𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧 ) → ∀ 𝑤 ( 𝑤 ∈ 𝑥 → ∀ 𝑥 𝑤 ∈ 𝑥 ) ) )
13	2 12	mpcom	⊢ ( ∀ 𝑥 ∀ 𝑤 ( 𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧 ) → ∀ 𝑤 ( 𝑤 ∈ 𝑥 → ∀ 𝑥 𝑤 ∈ 𝑥 ) )
14	13	axc4i	⊢ ( ∀ 𝑥 ∀ 𝑤 ( 𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧 ) → ∀ 𝑥 ∀ 𝑤 ( 𝑤 ∈ 𝑥 → ∀ 𝑥 𝑤 ∈ 𝑥 ) )
15		nfa1	⊢ Ⅎ 𝑥 ∀ 𝑥 𝑤 ∈ 𝑥
16	15	19.23	⊢ ( ∀ 𝑥 ( 𝑤 ∈ 𝑥 → ∀ 𝑥 𝑤 ∈ 𝑥 ) ↔ ( ∃ 𝑥 𝑤 ∈ 𝑥 → ∀ 𝑥 𝑤 ∈ 𝑥 ) )
17		19.8a	⊢ ( 𝑤 ∈ 𝑧 → ∃ 𝑧 𝑤 ∈ 𝑧 )
18		elequ2	⊢ ( 𝑧 = 𝑥 → ( 𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥 ) )
19	18	cbvexvw	⊢ ( ∃ 𝑧 𝑤 ∈ 𝑧 ↔ ∃ 𝑥 𝑤 ∈ 𝑥 )
20	17 19	sylib	⊢ ( 𝑤 ∈ 𝑧 → ∃ 𝑥 𝑤 ∈ 𝑥 )
21	4	cbvalivw	⊢ ( ∀ 𝑥 𝑤 ∈ 𝑥 → ∀ 𝑧 𝑤 ∈ 𝑧 )
22	20 21	imim12i	⊢ ( ( ∃ 𝑥 𝑤 ∈ 𝑥 → ∀ 𝑥 𝑤 ∈ 𝑥 ) → ( 𝑤 ∈ 𝑧 → ∀ 𝑧 𝑤 ∈ 𝑧 ) )
23	16 22	sylbi	⊢ ( ∀ 𝑥 ( 𝑤 ∈ 𝑥 → ∀ 𝑥 𝑤 ∈ 𝑥 ) → ( 𝑤 ∈ 𝑧 → ∀ 𝑧 𝑤 ∈ 𝑧 ) )
24	23	alimi	⊢ ( ∀ 𝑤 ∀ 𝑥 ( 𝑤 ∈ 𝑥 → ∀ 𝑥 𝑤 ∈ 𝑥 ) → ∀ 𝑤 ( 𝑤 ∈ 𝑧 → ∀ 𝑧 𝑤 ∈ 𝑧 ) )
25	24	alcoms	⊢ ( ∀ 𝑥 ∀ 𝑤 ( 𝑤 ∈ 𝑥 → ∀ 𝑥 𝑤 ∈ 𝑥 ) → ∀ 𝑤 ( 𝑤 ∈ 𝑧 → ∀ 𝑧 𝑤 ∈ 𝑧 ) )
26	25	alrimiv	⊢ ( ∀ 𝑥 ∀ 𝑤 ( 𝑤 ∈ 𝑥 → ∀ 𝑥 𝑤 ∈ 𝑥 ) → ∀ 𝑧 ∀ 𝑤 ( 𝑤 ∈ 𝑧 → ∀ 𝑧 𝑤 ∈ 𝑧 ) )
27		nfa1	⊢ Ⅎ 𝑧 ∀ 𝑧 𝑤 ∈ 𝑧
28	27	19.23	⊢ ( ∀ 𝑧 ( 𝑤 ∈ 𝑧 → ∀ 𝑧 𝑤 ∈ 𝑧 ) ↔ ( ∃ 𝑧 𝑤 ∈ 𝑧 → ∀ 𝑧 𝑤 ∈ 𝑧 ) )
29		ax9	⊢ ( 𝑧 = 𝑥 → ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) )
30	29	spimvw	⊢ ( ∀ 𝑧 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 )
31	17 30	imim12i	⊢ ( ( ∃ 𝑧 𝑤 ∈ 𝑧 → ∀ 𝑧 𝑤 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥 ) )
32		19.8a	⊢ ( 𝑤 ∈ 𝑥 → ∃ 𝑥 𝑤 ∈ 𝑥 )
33		elequ2	⊢ ( 𝑥 = 𝑧 → ( 𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧 ) )
34	33	cbvexvw	⊢ ( ∃ 𝑥 𝑤 ∈ 𝑥 ↔ ∃ 𝑧 𝑤 ∈ 𝑧 )
35	32 34	sylib	⊢ ( 𝑤 ∈ 𝑥 → ∃ 𝑧 𝑤 ∈ 𝑧 )
36		sp	⊢ ( ∀ 𝑧 𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑧 )
37	35 36	imim12i	⊢ ( ( ∃ 𝑧 𝑤 ∈ 𝑧 → ∀ 𝑧 𝑤 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑥 → 𝑤 ∈ 𝑧 ) )
38	31 37	impbid	⊢ ( ( ∃ 𝑧 𝑤 ∈ 𝑧 → ∀ 𝑧 𝑤 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥 ) )
39	28 38	sylbi	⊢ ( ∀ 𝑧 ( 𝑤 ∈ 𝑧 → ∀ 𝑧 𝑤 ∈ 𝑧 ) → ( 𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥 ) )
40	39	alimi	⊢ ( ∀ 𝑤 ∀ 𝑧 ( 𝑤 ∈ 𝑧 → ∀ 𝑧 𝑤 ∈ 𝑧 ) → ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥 ) )
41	40	alcoms	⊢ ( ∀ 𝑧 ∀ 𝑤 ( 𝑤 ∈ 𝑧 → ∀ 𝑧 𝑤 ∈ 𝑧 ) → ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥 ) )
42	41	axc4i	⊢ ( ∀ 𝑧 ∀ 𝑤 ( 𝑤 ∈ 𝑧 → ∀ 𝑧 𝑤 ∈ 𝑧 ) → ∀ 𝑧 ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥 ) )
43	14 26 42	3syl	⊢ ( ∀ 𝑥 ∀ 𝑤 ( 𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧 ) → ∀ 𝑧 ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥 ) )
44		axextb	⊢ ( 𝑥 = 𝑧 ↔ ∀ 𝑤 ( 𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧 ) )
45	44	albii	⊢ ( ∀ 𝑥 𝑥 = 𝑧 ↔ ∀ 𝑥 ∀ 𝑤 ( 𝑤 ∈ 𝑥 ↔ 𝑤 ∈ 𝑧 ) )
46		axextb	⊢ ( 𝑧 = 𝑥 ↔ ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥 ) )
47	46	albii	⊢ ( ∀ 𝑧 𝑧 = 𝑥 ↔ ∀ 𝑧 ∀ 𝑤 ( 𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑥 ) )
48	43 45 47	3imtr4i	⊢ ( ∀ 𝑥 𝑥 = 𝑧 → ∀ 𝑧 𝑧 = 𝑥 )