Theorem axacnd 10414

Description: A version of the Axiom of Choice with no distinct variable conditions. (New usage is discouraged.) (Contributed by NM, 3-Jan-2002.) (Proof shortened by Mario Carneiro, 10-Dec-2016.)

Assertion

Ref	Expression
axacnd	⊢ ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))

Proof of Theorem axacnd

Dummy variable 𝑣 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		axacndlem5 10413	. . . 4 ⊢ ∃𝑥∀𝑦∀𝑣(∀𝑥(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))
2		nfnae 2432	. . . . . 6 ⊢ Ⅎ𝑥 ¬ ∀𝑧 𝑧 = 𝑥
3		nfnae 2432	. . . . . 6 ⊢ Ⅎ𝑥 ¬ ∀𝑧 𝑧 = 𝑦
4		nfnae 2432	. . . . . 6 ⊢ Ⅎ𝑥 ¬ ∀𝑧 𝑧 = 𝑤
5	2, 3, 4	nf3an 1902	. . . . 5 ⊢ Ⅎ𝑥(¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤)
6		nfnae 2432	. . . . . . 7 ⊢ Ⅎ𝑦 ¬ ∀𝑧 𝑧 = 𝑥
7		nfnae 2432	. . . . . . 7 ⊢ Ⅎ𝑦 ¬ ∀𝑧 𝑧 = 𝑦
8		nfnae 2432	. . . . . . 7 ⊢ Ⅎ𝑦 ¬ ∀𝑧 𝑧 = 𝑤
9	6, 7, 8	nf3an 1902	. . . . . 6 ⊢ Ⅎ𝑦(¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤)
10		nfnae 2432	. . . . . . . 8 ⊢ Ⅎ𝑧 ¬ ∀𝑧 𝑧 = 𝑥
11		nfnae 2432	. . . . . . . 8 ⊢ Ⅎ𝑧 ¬ ∀𝑧 𝑧 = 𝑦
12		nfnae 2432	. . . . . . . 8 ⊢ Ⅎ𝑧 ¬ ∀𝑧 𝑧 = 𝑤
13	10, 11, 12	nf3an 1902	. . . . . . 7 ⊢ Ⅎ𝑧(¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤)
14		nfcvf 2934	. . . . . . . . . . . 12 ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧𝑦)
15	14	3ad2ant2 1134	. . . . . . . . . . 11 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧𝑦)
16		nfcvd 2906	. . . . . . . . . . 11 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧𝑣)
17	15, 16	nfeld 2916	. . . . . . . . . 10 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧 𝑦 ∈ 𝑣)
18		nfcvf 2934	. . . . . . . . . . . 12 ⊢ (¬ ∀𝑧 𝑧 = 𝑤 → Ⅎ𝑧𝑤)
19	18	3ad2ant3 1135	. . . . . . . . . . 11 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧𝑤)
20	16, 19	nfeld 2916	. . . . . . . . . 10 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧 𝑣 ∈ 𝑤)
21	17, 20	nfand 1898	. . . . . . . . 9 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤))
22	5, 21	nfald 2320	. . . . . . . 8 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧∀𝑥(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤))
23		nfnae 2432	. . . . . . . . . 10 ⊢ Ⅎ𝑤 ¬ ∀𝑧 𝑧 = 𝑥
24		nfnae 2432	. . . . . . . . . 10 ⊢ Ⅎ𝑤 ¬ ∀𝑧 𝑧 = 𝑦
25		nfnae 2432	. . . . . . . . . 10 ⊢ Ⅎ𝑤 ¬ ∀𝑧 𝑧 = 𝑤
26	23, 24, 25	nf3an 1902	. . . . . . . . 9 ⊢ Ⅎ𝑤(¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤)
27	15, 19	nfeld 2916	. . . . . . . . . . . . . 14 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧 𝑦 ∈ 𝑤)
28		nfcvf 2934	. . . . . . . . . . . . . . . 16 ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → Ⅎ𝑧𝑥)
29	28	3ad2ant1 1133	. . . . . . . . . . . . . . 15 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧𝑥)
30	19, 29	nfeld 2916	. . . . . . . . . . . . . 14 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧 𝑤 ∈ 𝑥)
31	27, 30	nfand 1898	. . . . . . . . . . . . 13 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧(𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥))
32	21, 31	nfand 1898	. . . . . . . . . . . 12 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)))
33	26, 32	nfexd 2321	. . . . . . . . . . 11 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)))
34	15, 19	nfeqd 2915	. . . . . . . . . . 11 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧 𝑦 = 𝑤)
35	33, 34	nfbid 1903	. . . . . . . . . 10 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))
36	9, 35	nfald 2320	. . . . . . . . 9 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧∀𝑦(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))
37	26, 36	nfexd 2321	. . . . . . . 8 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))
38	22, 37	nfimd 1895	. . . . . . 7 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧(∀𝑥(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
39		nfcvd 2906	. . . . . . . . . . . 12 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑥𝑣)
40		nfcvf2 2935	. . . . . . . . . . . . 13 ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → Ⅎ𝑥𝑧)
41	40	3ad2ant1 1133	. . . . . . . . . . . 12 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑥𝑧)
42	39, 41	nfeqd 2915	. . . . . . . . . . 11 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑥 𝑣 = 𝑧)
43	5, 42	nfan1 2191	. . . . . . . . . 10 ⊢ Ⅎ𝑥((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧)
44		simpr 486	. . . . . . . . . . . 12 ⊢ (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → 𝑣 = 𝑧)
45	44	eleq2d 2822	. . . . . . . . . . 11 ⊢ (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → (𝑦 ∈ 𝑣 ↔ 𝑦 ∈ 𝑧))
46	44	eleq1d 2821	. . . . . . . . . . 11 ⊢ (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → (𝑣 ∈ 𝑤 ↔ 𝑧 ∈ 𝑤))
47	45, 46	anbi12d 632	. . . . . . . . . 10 ⊢ (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → ((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ↔ (𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤)))
48	43, 47	albid 2213	. . . . . . . . 9 ⊢ (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → (∀𝑥(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ↔ ∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤)))
49		nfcvd 2906	. . . . . . . . . . . 12 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑤𝑣)
50		nfcvf2 2935	. . . . . . . . . . . . 13 ⊢ (¬ ∀𝑧 𝑧 = 𝑤 → Ⅎ𝑤𝑧)
51	50	3ad2ant3 1135	. . . . . . . . . . . 12 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑤𝑧)
52	49, 51	nfeqd 2915	. . . . . . . . . . 11 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑤 𝑣 = 𝑧)
53	26, 52	nfan1 2191	. . . . . . . . . 10 ⊢ Ⅎ𝑤((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧)
54		nfcvd 2906	. . . . . . . . . . . . 13 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑦𝑣)
55		nfcvf2 2935	. . . . . . . . . . . . . 14 ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑦𝑧)
56	55	3ad2ant2 1134	. . . . . . . . . . . . 13 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑦𝑧)
57	54, 56	nfeqd 2915	. . . . . . . . . . . 12 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑦 𝑣 = 𝑧)
58	9, 57	nfan1 2191	. . . . . . . . . . 11 ⊢ Ⅎ𝑦((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧)
59	47	anbi1d 631	. . . . . . . . . . . . 13 ⊢ (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → (((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥))))
60	53, 59	exbid 2214	. . . . . . . . . . . 12 ⊢ (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → (∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ ∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥))))
61	60	bibi1d 344	. . . . . . . . . . 11 ⊢ (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → ((∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤) ↔ (∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
62	58, 61	albid 2213	. . . . . . . . . 10 ⊢ (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → (∀𝑦(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤) ↔ ∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
63	53, 62	exbid 2214	. . . . . . . . 9 ⊢ (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → (∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤) ↔ ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
64	48, 63	imbi12d 345	. . . . . . . 8 ⊢ (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → ((∀𝑥(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)) ↔ (∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))))
65	64	ex 414	. . . . . . 7 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → (𝑣 = 𝑧 → ((∀𝑥(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)) ↔ (∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))))
66	13, 38, 65	cbvald 2405	. . . . . 6 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → (∀𝑣(∀𝑥(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)) ↔ ∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))))
67	9, 66	albid 2213	. . . . 5 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → (∀𝑦∀𝑣(∀𝑥(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)) ↔ ∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))))
68	5, 67	exbid 2214	. . . 4 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → (∃𝑥∀𝑦∀𝑣(∀𝑥(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)) ↔ ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))))
69	1, 68	mpbii 232	. . 3 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
70	69	3exp 1119	. 2 ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (¬ ∀𝑧 𝑧 = 𝑤 → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))))
71		axacndlem2 10410	. . 3 ⊢ (∀𝑥 𝑥 = 𝑧 → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
72	71	aecoms 2426	. 2 ⊢ (∀𝑧 𝑧 = 𝑥 → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
73		axacndlem3 10411	. . 3 ⊢ (∀𝑦 𝑦 = 𝑧 → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
74	73	aecoms 2426	. 2 ⊢ (∀𝑧 𝑧 = 𝑦 → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
75		nfae 2431	. . . 4 ⊢ Ⅎ𝑦∀𝑧 𝑧 = 𝑤
76		simpr 486	. . . . . . 7 ⊢ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → 𝑧 ∈ 𝑤)
77	76	alimi 1811	. . . . . 6 ⊢ (∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∀𝑥 𝑧 ∈ 𝑤)
78		nd3 10391	. . . . . . 7 ⊢ (∀𝑧 𝑧 = 𝑤 → ¬ ∀𝑥 𝑧 ∈ 𝑤)
79	78	pm2.21d 121	. . . . . 6 ⊢ (∀𝑧 𝑧 = 𝑤 → (∀𝑥 𝑧 ∈ 𝑤 → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
80	77, 79	syl5 34	. . . . 5 ⊢ (∀𝑧 𝑧 = 𝑤 → (∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
81	80	axc4i 2314	. . . 4 ⊢ (∀𝑧 𝑧 = 𝑤 → ∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
82	75, 81	alrimi 2204	. . 3 ⊢ (∀𝑧 𝑧 = 𝑤 → ∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
83	82	19.8ad 2173	. 2 ⊢ (∀𝑧 𝑧 = 𝑤 → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
84	70, 72, 74, 83	pm2.61iii 185	1 ⊢ ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1087  ∀wal 1537  ∃wex 1779  Ⅎwnfc 2885

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-13 2370  ax-ext 2707  ax-sep 5232  ax-nul 5239  ax-pr 5361  ax-reg 9395  ax-ac 10261

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 846  df-3an 1089  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3287  df-v 3439  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4566  df-pr 4568  df-op 4572  df-br 5082  df-opab 5144  df-eprel 5506  df-fr 5555

This theorem is referenced by:  zfcndac  10421  axacprim  33693