Theorem axacnd 10567

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 10566	. . . 4 ⊢ ∃𝑥∀𝑦∀𝑣(∀𝑥(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))
2		nfnae 2464	. . . . . 6 ⊢ Ⅎ𝑥 ¬ ∀𝑧 𝑧 = 𝑥
3		nfnae 2464	. . . . . 6 ⊢ Ⅎ𝑥 ¬ ∀𝑧 𝑧 = 𝑦
4		nfnae 2464	. . . . . 6 ⊢ Ⅎ𝑥 ¬ ∀𝑧 𝑧 = 𝑤
5	2, 3, 4	nf3an 1920	. . . . 5 ⊢ Ⅎ𝑥(¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤)
6		nfnae 2464	. . . . . . 7 ⊢ Ⅎ𝑦 ¬ ∀𝑧 𝑧 = 𝑥
7		nfnae 2464	. . . . . . 7 ⊢ Ⅎ𝑦 ¬ ∀𝑧 𝑧 = 𝑦
8		nfnae 2464	. . . . . . 7 ⊢ Ⅎ𝑦 ¬ ∀𝑧 𝑧 = 𝑤
9	6, 7, 8	nf3an 1920	. . . . . 6 ⊢ Ⅎ𝑦(¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤)
10		nfnae 2464	. . . . . . . 8 ⊢ Ⅎ𝑧 ¬ ∀𝑧 𝑧 = 𝑥
11		nfnae 2464	. . . . . . . 8 ⊢ Ⅎ𝑧 ¬ ∀𝑧 𝑧 = 𝑦
12		nfnae 2464	. . . . . . . 8 ⊢ Ⅎ𝑧 ¬ ∀𝑧 𝑧 = 𝑤
13	10, 11, 12	nf3an 1920	. . . . . . 7 ⊢ Ⅎ𝑧(¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤)
14		nfcvf 2949	. . . . . . . . . . . 12 ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧𝑦)
15	14	3ad2ant2 1146	. . . . . . . . . . 11 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧𝑦)
16		nfcvd 2924	. . . . . . . . . . 11 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧𝑣)
17	15, 16	nfeld 2934	. . . . . . . . . 10 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧 𝑦 ∈ 𝑣)
18		nfcvf 2949	. . . . . . . . . . . 12 ⊢ (¬ ∀𝑧 𝑧 = 𝑤 → Ⅎ𝑧𝑤)
19	18	3ad2ant3 1147	. . . . . . . . . . 11 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧𝑤)
20	16, 19	nfeld 2934	. . . . . . . . . 10 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧 𝑣 ∈ 𝑤)
21	17, 20	nfand 1916	. . . . . . . . 9 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤))
22	5, 21	nfald 2359	. . . . . . . 8 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧∀𝑥(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤))
23		nfnae 2464	. . . . . . . . . 10 ⊢ Ⅎ𝑤 ¬ ∀𝑧 𝑧 = 𝑥
24		nfnae 2464	. . . . . . . . . 10 ⊢ Ⅎ𝑤 ¬ ∀𝑧 𝑧 = 𝑦
25		nfnae 2464	. . . . . . . . . 10 ⊢ Ⅎ𝑤 ¬ ∀𝑧 𝑧 = 𝑤
26	23, 24, 25	nf3an 1920	. . . . . . . . 9 ⊢ Ⅎ𝑤(¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤)
27	15, 19	nfeld 2934	. . . . . . . . . . . . . 14 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧 𝑦 ∈ 𝑤)
28		nfcvf 2949	. . . . . . . . . . . . . . . 16 ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → Ⅎ𝑧𝑥)
29	28	3ad2ant1 1145	. . . . . . . . . . . . . . 15 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧𝑥)
30	19, 29	nfeld 2934	. . . . . . . . . . . . . 14 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧 𝑤 ∈ 𝑥)
31	27, 30	nfand 1916	. . . . . . . . . . . . 13 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧(𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥))
32	21, 31	nfand 1916	. . . . . . . . . . . 12 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)))
33	26, 32	nfexd 2360	. . . . . . . . . . 11 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)))
34	15, 19	nfeqd 2933	. . . . . . . . . . 11 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧 𝑦 = 𝑤)
35	33, 34	nfbid 1921	. . . . . . . . . 10 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))
36	9, 35	nfald 2359	. . . . . . . . 9 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧∀𝑦(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))
37	26, 36	nfexd 2360	. . . . . . . 8 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))
38	22, 37	nfimd 1913	. . . . . . 7 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑧(∀𝑥(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
39		nfcvd 2924	. . . . . . . . . . . 12 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑥𝑣)
40		nfcvf2 2950	. . . . . . . . . . . . 13 ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → Ⅎ𝑥𝑧)
41	40	3ad2ant1 1145	. . . . . . . . . . . 12 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑥𝑧)
42	39, 41	nfeqd 2933	. . . . . . . . . . 11 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑥 𝑣 = 𝑧)
43	5, 42	nfan1 2234	. . . . . . . . . 10 ⊢ Ⅎ𝑥((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧)
44		simpr 488	. . . . . . . . . . . 12 ⊢ (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → 𝑣 = 𝑧)
45	44	eleq2d 2847	. . . . . . . . . . 11 ⊢ (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → (𝑦 ∈ 𝑣 ↔ 𝑦 ∈ 𝑧))
46	44	eleq1d 2846	. . . . . . . . . . 11 ⊢ (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → (𝑣 ∈ 𝑤 ↔ 𝑧 ∈ 𝑤))
47	45, 46	anbi12d 641	. . . . . . . . . 10 ⊢ (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → ((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ↔ (𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤)))
48	43, 47	albid 2256	. . . . . . . . 9 ⊢ (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → (∀𝑥(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ↔ ∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤)))
49		nfcvd 2924	. . . . . . . . . . . 12 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑤𝑣)
50		nfcvf2 2950	. . . . . . . . . . . . 13 ⊢ (¬ ∀𝑧 𝑧 = 𝑤 → Ⅎ𝑤𝑧)
51	50	3ad2ant3 1147	. . . . . . . . . . . 12 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑤𝑧)
52	49, 51	nfeqd 2933	. . . . . . . . . . 11 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑤 𝑣 = 𝑧)
53	26, 52	nfan1 2234	. . . . . . . . . 10 ⊢ Ⅎ𝑤((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧)
54		nfcvd 2924	. . . . . . . . . . . . 13 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑦𝑣)
55		nfcvf2 2950	. . . . . . . . . . . . . 14 ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑦𝑧)
56	55	3ad2ant2 1146	. . . . . . . . . . . . 13 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑦𝑧)
57	54, 56	nfeqd 2933	. . . . . . . . . . . 12 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → Ⅎ𝑦 𝑣 = 𝑧)
58	9, 57	nfan1 2234	. . . . . . . . . . 11 ⊢ Ⅎ𝑦((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧)
59	47	anbi1d 640	. . . . . . . . . . . . 13 ⊢ (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → (((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥))))
60	53, 59	exbid 2257	. . . . . . . . . . . 12 ⊢ (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → (∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ ∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥))))
61	60	bibi1d 345	. . . . . . . . . . 11 ⊢ (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → ((∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤) ↔ (∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
62	58, 61	albid 2256	. . . . . . . . . 10 ⊢ (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → (∀𝑦(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤) ↔ ∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
63	53, 62	exbid 2257	. . . . . . . . 9 ⊢ (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → (∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤) ↔ ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
64	48, 63	imbi12d 346	. . . . . . . 8 ⊢ (((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) ∧ 𝑣 = 𝑧) → ((∀𝑥(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)) ↔ (∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))))
65	64	ex 416	. . . . . . 7 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → (𝑣 = 𝑧 → ((∀𝑥(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)) ↔ (∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))))
66	13, 38, 65	cbvald 2437	. . . . . 6 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → (∀𝑣(∀𝑥(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)) ↔ ∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))))
67	9, 66	albid 2256	. . . . 5 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → (∀𝑦∀𝑣(∀𝑥(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)) ↔ ∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))))
68	5, 67	exbid 2257	. . . 4 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → (∃𝑥∀𝑦∀𝑣(∀𝑥(𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑣 ∧ 𝑣 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)) ↔ ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))))
69	1, 68	mpbii 235	. . 3 ⊢ ((¬ ∀𝑧 𝑧 = 𝑥 ∧ ¬ ∀𝑧 𝑧 = 𝑦 ∧ ¬ ∀𝑧 𝑧 = 𝑤) → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
70	69	3exp 1131	. 2 ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → (¬ ∀𝑧 𝑧 = 𝑦 → (¬ ∀𝑧 𝑧 = 𝑤 → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))))
71		axacndlem2 10563	. . 3 ⊢ (∀𝑥 𝑥 = 𝑧 → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
72	71	aecoms 2458	. 2 ⊢ (∀𝑧 𝑧 = 𝑥 → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
73		axacndlem3 10564	. . 3 ⊢ (∀𝑦 𝑦 = 𝑧 → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
74	73	aecoms 2458	. 2 ⊢ (∀𝑧 𝑧 = 𝑦 → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
75		nfae 2463	. . . 4 ⊢ Ⅎ𝑦∀𝑧 𝑧 = 𝑤
76		simpr 488	. . . . . . 7 ⊢ ((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → 𝑧 ∈ 𝑤)
77	76	alimi 1830	. . . . . 6 ⊢ (∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∀𝑥 𝑧 ∈ 𝑤)
78		nd3 10544	. . . . . . 7 ⊢ (∀𝑧 𝑧 = 𝑤 → ¬ ∀𝑥 𝑧 ∈ 𝑤)
79	78	pm2.21d 121	. . . . . 6 ⊢ (∀𝑧 𝑧 = 𝑤 → (∀𝑥 𝑧 ∈ 𝑤 → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
80	77, 79	syl5 34	. . . . 5 ⊢ (∀𝑧 𝑧 = 𝑤 → (∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
81	80	axc4i 2353	. . . 4 ⊢ (∀𝑧 𝑧 = 𝑤 → ∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
82	75, 81	alrimi 2247	. . 3 ⊢ (∀𝑧 𝑧 = 𝑤 → ∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
83	82	19.8ad 2216	. 2 ⊢ (∀𝑧 𝑧 = 𝑤 → ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤)))
84	70, 72, 74, 83	pm2.61iii 186	1 ⊢ ∃𝑥∀𝑦∀𝑧(∀𝑥(𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) → ∃𝑤∀𝑦(∃𝑤((𝑦 ∈ 𝑧 ∧ 𝑧 ∈ 𝑤) ∧ (𝑦 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥)) ↔ 𝑦 = 𝑤))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 399   ∧ w3a 1097  ∀wal 1557  ∃wex 1798  Ⅎwnfc 2908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-13 2402  ax-ext 2733  ax-sep 5245  ax-pr 5389  ax-reg 9537  ax-ac 10413

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-pw 4556  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-eprel 5545  df-fr 5598

This theorem is referenced by:  zfcndac  10574  axacprim  36021