Theorem axacnd 10352

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 10351	. . . 4 ⊢ ∃𝑥∀𝑦∀𝑣(∀𝑥(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))
2		nfnae 2435	. . . . . 6 ⊢ Ⅎ𝑥 ¬ ∀𝑧 𝑧 = 𝑥
3		nfnae 2435	. . . . . 6 ⊢ Ⅎ𝑥 ¬ ∀𝑧 𝑧 = 𝑦
4		nfnae 2435	. . . . . 6 ⊢ Ⅎ𝑥 ¬ ∀𝑧 𝑧 = 𝑤
5	2, 3, 4	nf3an 1907	. . . . 5 ⊢ Ⅎ𝑥(¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤)
6		nfnae 2435	. . . . . . 7 ⊢ Ⅎ𝑦 ¬ ∀𝑧 𝑧 = 𝑥
7		nfnae 2435	. . . . . . 7 ⊢ Ⅎ𝑦 ¬ ∀𝑧 𝑧 = 𝑦
8		nfnae 2435	. . . . . . 7 ⊢ Ⅎ𝑦 ¬ ∀𝑧 𝑧 = 𝑤
9	6, 7, 8	nf3an 1907	. . . . . 6 ⊢ Ⅎ𝑦(¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤)
10		nfnae 2435	. . . . . . . 8 ⊢ Ⅎ𝑧 ¬ ∀𝑧 𝑧 = 𝑥
11		nfnae 2435	. . . . . . . 8 ⊢ Ⅎ𝑧 ¬ ∀𝑧 𝑧 = 𝑦
12		nfnae 2435	. . . . . . . 8 ⊢ Ⅎ𝑧 ¬ ∀𝑧 𝑧 = 𝑤
13	10, 11, 12	nf3an 1907	. . . . . . 7 ⊢ Ⅎ𝑧(¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤)
14		nfcvf 2937	. . . . . . . . . . . 12 ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧𝑦)
15	14	3ad2ant2 1132	. . . . . . . . . . 11 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧𝑦)
16		nfcvd 2909	. . . . . . . . . . 11 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧𝑣)
17	15, 16	nfeld 2919	. . . . . . . . . 10 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧 𝑦 ∈ 𝑣)
18		nfcvf 2937	. . . . . . . . . . . 12 ⊢ (¬ ∀𝑧 𝑧 = 𝑤 → Ⅎ𝑧𝑤)
19	18	3ad2ant3 1133	. . . . . . . . . . 11 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧𝑤)
20	16, 19	nfeld 2919	. . . . . . . . . 10 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧 𝑣 ∈ 𝑤)
21	17, 20	nfand 1903	. . . . . . . . 9 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤))
22	5, 21	nfald 2325	. . . . . . . 8 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧∀𝑥(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤))
23		nfnae 2435	. . . . . . . . . 10 ⊢ Ⅎ𝑤 ¬ ∀𝑧 𝑧 = 𝑥
24		nfnae 2435	. . . . . . . . . 10 ⊢ Ⅎ𝑤 ¬ ∀𝑧 𝑧 = 𝑦
25		nfnae 2435	. . . . . . . . . 10 ⊢ Ⅎ𝑤 ¬ ∀𝑧 𝑧 = 𝑤
26	23, 24, 25	nf3an 1907	. . . . . . . . 9 ⊢ Ⅎ𝑤(¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤)
27	15, 19	nfeld 2919	. . . . . . . . . . . . . 14 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧 𝑦 ∈ 𝑤)
28		nfcvf 2937	. . . . . . . . . . . . . . . 16 ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → Ⅎ𝑧𝑥)
29	28	3ad2ant1 1131	. . . . . . . . . . . . . . 15 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧𝑥)
30	19, 29	nfeld 2919	. . . . . . . . . . . . . 14 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧 𝑤 ∈ 𝑥)
31	27, 30	nfand 1903	. . . . . . . . . . . . 13 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧(𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥))
32	21, 31	nfand 1903	. . . . . . . . . . . 12 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)))
33	26, 32	nfexd 2326	. . . . . . . . . . 11 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)))
34	15, 19	nfeqd 2918	. . . . . . . . . . 11 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧 𝑦 = 𝑤)
35	33, 34	nfbid 1908	. . . . . . . . . 10 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))
36	9, 35	nfald 2325	. . . . . . . . 9 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧∀𝑦(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))
37	26, 36	nfexd 2326	. . . . . . . 8 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))
38	22, 37	nfimd 1900	. . . . . . 7 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧(∀𝑥(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
39		nfcvd 2909	. . . . . . . . . . . 12 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑥𝑣)
40		nfcvf2 2938	. . . . . . . . . . . . 13 ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → Ⅎ𝑥𝑧)
41	40	3ad2ant1 1131	. . . . . . . . . . . 12 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑥𝑧)
42	39, 41	nfeqd 2918	. . . . . . . . . . 11 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑥 𝑣 = 𝑧)
43	5, 42	nfan1 2196	. . . . . . . . . 10 ⊢ Ⅎ𝑥((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧)
44		simpr 484	. . . . . . . . . . . 12 ⊢ (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → 𝑣 = 𝑧)
45	44	eleq2d 2825	. . . . . . . . . . 11 ⊢ (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → (𝑦 ∈ 𝑣 ↔ 𝑦 ∈ 𝑧))
46	44	eleq1d 2824	. . . . . . . . . . 11 ⊢ (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → (𝑣 ∈ 𝑤 ↔ 𝑧 ∈ 𝑤))
47	45, 46	anbi12d 630	. . . . . . . . . 10 ⊢ (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → ((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ↔ (𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤)))
48	43, 47	albid 2218	. . . . . . . . 9 ⊢ (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → (∀𝑥(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ↔ ∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤)))
49		nfcvd 2909	. . . . . . . . . . . 12 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑤𝑣)
50		nfcvf2 2938	. . . . . . . . . . . . 13 ⊢ (¬ ∀𝑧 𝑧 = 𝑤 → Ⅎ𝑤𝑧)
51	50	3ad2ant3 1133	. . . . . . . . . . . 12 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑤𝑧)
52	49, 51	nfeqd 2918	. . . . . . . . . . 11 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑤 𝑣 = 𝑧)
53	26, 52	nfan1 2196	. . . . . . . . . 10 ⊢ Ⅎ𝑤((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧)
54		nfcvd 2909	. . . . . . . . . . . . 13 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑦𝑣)
55		nfcvf2 2938	. . . . . . . . . . . . . 14 ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑦𝑧)
56	55	3ad2ant2 1132	. . . . . . . . . . . . 13 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑦𝑧)
57	54, 56	nfeqd 2918	. . . . . . . . . . . 12 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑦 𝑣 = 𝑧)
58	9, 57	nfan1 2196	. . . . . . . . . . 11 ⊢ Ⅎ𝑦((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧)
59	47	anbi1d 629	. . . . . . . . . . . . 13 ⊢ (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → (((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥))))
60	53, 59	exbid 2219	. . . . . . . . . . . 12 ⊢ (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → (∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ ∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥))))
61	60	bibi1d 343	. . . . . . . . . . 11 ⊢ (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → ((∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤) ↔ (∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
62	58, 61	albid 2218	. . . . . . . . . 10 ⊢ (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → (∀𝑦(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤) ↔ ∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
63	53, 62	exbid 2219	. . . . . . . . 9 ⊢ (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → (∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤) ↔ ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
64	48, 63	imbi12d 344	. . . . . . . 8 ⊢ (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → ((∀𝑥(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)) ↔ (∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))))
65	64	ex 412	. . . . . . 7 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → (𝑣 = 𝑧 → ((∀𝑥(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)) ↔ (∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))))
66	13, 38, 65	cbvald 2408	. . . . . 6 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → (∀𝑣(∀𝑥(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)) ↔ ∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))))
67	9, 66	albid 2218	. . . . 5 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → (∀𝑦∀𝑣(∀𝑥(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)) ↔ ∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))))
68	5, 67	exbid 2219	. . . 4 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → (∃𝑥∀𝑦∀𝑣(∀𝑥(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)) ↔ ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))))
69	1, 68	mpbii 232	. . 3 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
70	69	3exp 1117	. 2 ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (¬ ∀𝑧 𝑧 = 𝑤 → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))))
71		axacndlem2 10348	. . 3 ⊢ (∀𝑥 𝑥 = 𝑧 → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
72	71	aecoms 2429	. 2 ⊢ (∀𝑧 𝑧 = 𝑥 → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
73		axacndlem3 10349	. . 3 ⊢ (∀𝑦 𝑦 = 𝑧 → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
74	73	aecoms 2429	. 2 ⊢ (∀𝑧 𝑧 = 𝑦 → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
75		nfae 2434	. . . 4 ⊢ Ⅎ𝑦∀𝑧 𝑧 = 𝑤
76		simpr 484	. . . . . . 7 ⊢ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → 𝑧 ∈ 𝑤)
77	76	alimi 1817	. . . . . 6 ⊢ (∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∀𝑥 𝑧 ∈ 𝑤)
78		nd3 10329	. . . . . . 7 ⊢ (∀𝑧 𝑧 = 𝑤 → ¬ ∀𝑥 𝑧 ∈ 𝑤)
79	78	pm2.21d 121	. . . . . 6 ⊢ (∀𝑧 𝑧 = 𝑤 → (∀𝑥 𝑧 ∈ 𝑤 → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
80	77, 79	syl5 34	. . . . 5 ⊢ (∀𝑧 𝑧 = 𝑤 → (∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
81	80	axc4i 2319	. . . 4 ⊢ (∀𝑧 𝑧 = 𝑤 → ∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
82	75, 81	alrimi 2209	. . 3 ⊢ (∀𝑧 𝑧 = 𝑤 → ∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
83	82	19.8ad 2178	. 2 ⊢ (∀𝑧 𝑧 = 𝑤 → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
84	70, 72, 74, 83	pm2.61iii 185	1 ⊢ ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085  ∀wal 1539  ∃wex 1785  Ⅎwnfc 2888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-13 2373  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355  ax-reg 9312  ax-ac 10199

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ne 2945  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-pw 4540  df-sn 4567  df-pr 4569  df-op 4573  df-br 5079  df-opab 5141  df-eprel 5494  df-fr 5543

This theorem is referenced by:  zfcndac  10359  axacprim  33627