Theorem axtcond 37266

Description: A version of the Axiom of Transitive Containment with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 2401. (Contributed by Matthew House, 6-Apr-2026.) (New usage is discouraged.)

Assertion

Ref	Expression
axtcond	⊢ ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))

Proof of Theorem axtcond

Dummy variables 𝑢 𝑡 𝑣 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		axtco2 37262	. . . 4 ⊢ ∃𝑤∀𝑣((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤))
2		nfnae 2463	. . . . . 6 ⊢ Ⅎ𝑦 ¬ ∀𝑥 𝑥 = 𝑦
3		nfnae 2463	. . . . . 6 ⊢ Ⅎ𝑦 ¬ ∀𝑥 𝑥 = 𝑧
4		nfnae 2463	. . . . . 6 ⊢ Ⅎ𝑦 ¬ ∀𝑦 𝑦 = 𝑧
5	2, 3, 4	nf3an 1933	. . . . 5 ⊢ Ⅎ𝑦(¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧)
6		nfv 1946	. . . . . . . 8 ⊢ Ⅎ𝑦∀𝑣((𝑣 = 𝑡 ∨ 𝑣 ∈ 𝑤) → ∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑤))
7		equequ2 2058	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑥 → (𝑣 = 𝑡 ↔ 𝑣 = 𝑥))
8	7	orbi1d 930	. . . . . . . . . 10 ⊢ (𝑡 = 𝑥 → ((𝑣 = 𝑡 ∨ 𝑣 ∈ 𝑤) ↔ (𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤)))
9		elequ1 2151	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑥 → (𝑡 ∈ 𝑣 ↔ 𝑥 ∈ 𝑣))
10		elequ1 2151	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑥 → (𝑡 ∈ 𝑤 ↔ 𝑥 ∈ 𝑤))
11	9, 10	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑥 → ((𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑤) ↔ (𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)))
12	11	cbvalvw 2068	. . . . . . . . . . 11 ⊢ (∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑤) ↔ ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤))
13	12	a1i 11	. . . . . . . . . 10 ⊢ (𝑡 = 𝑥 → (∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑤) ↔ ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)))
14	8, 13	imbi12d 347	. . . . . . . . 9 ⊢ (𝑡 = 𝑥 → (((𝑣 = 𝑡 ∨ 𝑣 ∈ 𝑤) → ∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑤)) ↔ ((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤))))
15	14	albidv 1952	. . . . . . . 8 ⊢ (𝑡 = 𝑥 → (∀𝑣((𝑣 = 𝑡 ∨ 𝑣 ∈ 𝑤) → ∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑤)) ↔ ∀𝑣((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤))))
16	6, 15	dvelimnf 2482	. . . . . . 7 ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → Ⅎ𝑦∀𝑣((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)))
17	16	naecoms 2458	. . . . . 6 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦∀𝑣((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)))
18	17	3ad2ant1 1151	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑦∀𝑣((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)))
19		nfnae 2463	. . . . . . . . 9 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦
20		nfnae 2463	. . . . . . . . 9 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑧
21		nfnae 2463	. . . . . . . . 9 ⊢ Ⅎ𝑧 ¬ ∀𝑦 𝑦 = 𝑧
22	19, 20, 21	nf3an 1933	. . . . . . . 8 ⊢ Ⅎ𝑧(¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧)
23		nfeqf2 2406	. . . . . . . . . 10 ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧 𝑤 = 𝑦)
24	23	naecoms 2458	. . . . . . . . 9 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧 𝑤 = 𝑦)
25	24	3ad2ant3 1153	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑧 𝑤 = 𝑦)
26	22, 25	nfan1 2236	. . . . . . 7 ⊢ Ⅎ𝑧((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦)
27		simpl2 1211	. . . . . . . 8 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) → ¬ ∀𝑥 𝑥 = 𝑧)
28		nfv 1946	. . . . . . . . . 10 ⊢ Ⅎ𝑧((𝑣 = 𝑡 ∨ 𝑣 ∈ 𝑤) → ∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑤))
29	28, 14	dvelimnf 2482	. . . . . . . . 9 ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → Ⅎ𝑧((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)))
30	29	naecoms 2458	. . . . . . . 8 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → Ⅎ𝑧((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)))
31	27, 30	syl 18	. . . . . . 7 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) → Ⅎ𝑧((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)))
32		equequ1 2057	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑧 → (𝑣 = 𝑥 ↔ 𝑧 = 𝑥))
33	32	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝑤 = 𝑦 ∧ 𝑣 = 𝑧) → (𝑣 = 𝑥 ↔ 𝑧 = 𝑥))
34		elequ12 2162	. . . . . . . . . . . . 13 ⊢ ((𝑣 = 𝑧 ∧ 𝑤 = 𝑦) → (𝑣 ∈ 𝑤 ↔ 𝑧 ∈ 𝑦))
35	34	ancoms 464	. . . . . . . . . . . 12 ⊢ ((𝑤 = 𝑦 ∧ 𝑣 = 𝑧) → (𝑣 ∈ 𝑤 ↔ 𝑧 ∈ 𝑦))
36	33, 35	orbi12d 932	. . . . . . . . . . 11 ⊢ ((𝑤 = 𝑦 ∧ 𝑣 = 𝑧) → ((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) ↔ (𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦)))
37	36	adantl 487	. . . . . . . . . 10 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ (𝑤 = 𝑦 ∧ 𝑣 = 𝑧)) → ((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) ↔ (𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦)))
38		nfnae 2463	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥 ¬ ∀𝑥 𝑥 = 𝑦
39		nfnae 2463	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥 ¬ ∀𝑥 𝑥 = 𝑧
40	38, 39	nfan 1931	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧)
41		nfeqf2 2406	. . . . . . . . . . . . . 14 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑤 = 𝑦)
42	41	adantr 486	. . . . . . . . . . . . 13 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑤 = 𝑦)
43		nfeqf2 2406	. . . . . . . . . . . . . 14 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥 𝑣 = 𝑧)
44	43	adantl 487	. . . . . . . . . . . . 13 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑣 = 𝑧)
45	42, 44	nfand 1929	. . . . . . . . . . . 12 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥(𝑤 = 𝑦 ∧ 𝑣 = 𝑧))
46	40, 45	nfan1 2236	. . . . . . . . . . 11 ⊢ Ⅎ𝑥((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ (𝑤 = 𝑦 ∧ 𝑣 = 𝑧))
47		elequ2 2159	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑧 → (𝑥 ∈ 𝑣 ↔ 𝑥 ∈ 𝑧))
48	47	adantl 487	. . . . . . . . . . . . 13 ⊢ ((𝑤 = 𝑦 ∧ 𝑣 = 𝑧) → (𝑥 ∈ 𝑣 ↔ 𝑥 ∈ 𝑧))
49		elequ2 2159	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑦 → (𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑦))
50	49	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝑤 = 𝑦 ∧ 𝑣 = 𝑧) → (𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑦))
51	48, 50	imbi12d 347	. . . . . . . . . . . 12 ⊢ ((𝑤 = 𝑦 ∧ 𝑣 = 𝑧) → ((𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤) ↔ (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
52	51	adantl 487	. . . . . . . . . . 11 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ (𝑤 = 𝑦 ∧ 𝑣 = 𝑧)) → ((𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤) ↔ (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
53	46, 52	albid 2258	. . . . . . . . . 10 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ (𝑤 = 𝑦 ∧ 𝑣 = 𝑧)) → (∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤) ↔ ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
54	37, 53	imbi12d 347	. . . . . . . . 9 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ (𝑤 = 𝑦 ∧ 𝑣 = 𝑧)) → (((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)) ↔ ((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))))
55	54	expr 462	. . . . . . . 8 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑦) → (𝑣 = 𝑧 → (((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)) ↔ ((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))))
56	55	3adantl3 1187	. . . . . . 7 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) → (𝑣 = 𝑧 → (((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)) ↔ ((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))))
57	26, 31, 56	cbvaldw 2367	. . . . . 6 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) → (∀𝑣((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)) ↔ ∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))))
58	57	ex 418	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (𝑤 = 𝑦 → (∀𝑣((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)) ↔ ∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))))
59	5, 18, 58	cbvexdw 2368	. . . 4 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (∃𝑤∀𝑣((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)) ↔ ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))))
60	1, 59	mpbii 236	. . 3 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
61	60	3exp 1137	. 2 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑦 𝑦 = 𝑧 → ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))))
62		nfae 2462	. . . . . 6 ⊢ Ⅎ𝑧∀𝑦 𝑦 = 𝑧
63		nfae 2462	. . . . . . . 8 ⊢ Ⅎ𝑥∀𝑦 𝑦 = 𝑧
64		elequ2 2159	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧))
65	64	sps 2221	. . . . . . . . 9 ⊢ (∀𝑦 𝑦 = 𝑧 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧))
66	65	biimprd 251	. . . . . . . 8 ⊢ (∀𝑦 𝑦 = 𝑧 → (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))
67	63, 66	alrimi 2249	. . . . . . 7 ⊢ (∀𝑦 𝑦 = 𝑧 → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))
68	67	a1d 26	. . . . . 6 ⊢ (∀𝑦 𝑦 = 𝑧 → ((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
69	62, 68	alrimi 2249	. . . . 5 ⊢ (∀𝑦 𝑦 = 𝑧 → ∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
70	69	19.8ad 2218	. . . 4 ⊢ (∀𝑦 𝑦 = 𝑧 → ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
71	70	a1i 11	. . 3 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦 𝑦 = 𝑧 → ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))))
72		ax-nul 5259	. . . . 5 ⊢ ∃𝑦∀𝑢 ¬ 𝑢 ∈ 𝑦
73		nfv 1946	. . . . . . . . 9 ⊢ Ⅎ𝑧∀𝑢 ¬ 𝑢 ∈ 𝑡
74		elequ2 2159	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑦 → (𝑢 ∈ 𝑡 ↔ 𝑢 ∈ 𝑦))
75	74	notbid 321	. . . . . . . . . 10 ⊢ (𝑡 = 𝑦 → (¬ 𝑢 ∈ 𝑡 ↔ ¬ 𝑢 ∈ 𝑦))
76	75	albidv 1952	. . . . . . . . 9 ⊢ (𝑡 = 𝑦 → (∀𝑢 ¬ 𝑢 ∈ 𝑡 ↔ ∀𝑢 ¬ 𝑢 ∈ 𝑦))
77	73, 76	dvelimnf 2482	. . . . . . . 8 ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧∀𝑢 ¬ 𝑢 ∈ 𝑦)
78	77	naecoms 2458	. . . . . . 7 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧∀𝑢 ¬ 𝑢 ∈ 𝑦)
79		elequ2 2159	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (𝑢 ∈ 𝑧 ↔ 𝑢 ∈ 𝑦))
80	79	notbid 321	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑦 → (¬ 𝑢 ∈ 𝑧 ↔ ¬ 𝑢 ∈ 𝑦))
81	80	albidv 1952	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑦 → (∀𝑢 ¬ 𝑢 ∈ 𝑧 ↔ ∀𝑢 ¬ 𝑢 ∈ 𝑦))
82	81	biimprcd 253	. . . . . . . . . 10 ⊢ (∀𝑢 ¬ 𝑢 ∈ 𝑦 → (𝑧 = 𝑦 → ∀𝑢 ¬ 𝑢 ∈ 𝑧))
83		elirrv 9591	. . . . . . . . . . . . . . 15 ⊢ ¬ 𝑥 ∈ 𝑥
84		elequ2 2159	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝑥 ↔ 𝑥 ∈ 𝑧))
85	83, 84	mtbii 329	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑧 → ¬ 𝑥 ∈ 𝑧)
86	85	pm2.21d 122	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))
87	86	alimi 1843	. . . . . . . . . . . 12 ⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))
88	87	a1d 26	. . . . . . . . . . 11 ⊢ (∀𝑥 𝑥 = 𝑧 → (∀𝑢 ¬ 𝑢 ∈ 𝑧 → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
89		nfv 1946	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥∀𝑢 ¬ 𝑢 ∈ 𝑡
90		elequ2 2159	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑧 → (𝑢 ∈ 𝑡 ↔ 𝑢 ∈ 𝑧))
91	90	notbid 321	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑧 → (¬ 𝑢 ∈ 𝑡 ↔ ¬ 𝑢 ∈ 𝑧))
92	91	albidv 1952	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑧 → (∀𝑢 ¬ 𝑢 ∈ 𝑡 ↔ ∀𝑢 ¬ 𝑢 ∈ 𝑧))
93	89, 92	dvelimnf 2482	. . . . . . . . . . . 12 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥∀𝑢 ¬ 𝑢 ∈ 𝑧)
94		elequ1 2151	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑥 → (𝑢 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧))
95	94	notbid 321	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑥 → (¬ 𝑢 ∈ 𝑧 ↔ ¬ 𝑥 ∈ 𝑧))
96	95	spvv 2020	. . . . . . . . . . . . . 14 ⊢ (∀𝑢 ¬ 𝑢 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑧)
97	96	pm2.21d 122	. . . . . . . . . . . . 13 ⊢ (∀𝑢 ¬ 𝑢 ∈ 𝑧 → (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))
98	97	a1i 11	. . . . . . . . . . . 12 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → (∀𝑢 ¬ 𝑢 ∈ 𝑧 → (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
99	39, 93, 98	alrimdd 2250	. . . . . . . . . . 11 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → (∀𝑢 ¬ 𝑢 ∈ 𝑧 → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
100	88, 99	pm2.61i 184	. . . . . . . . . 10 ⊢ (∀𝑢 ¬ 𝑢 ∈ 𝑧 → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))
101	82, 100	syl6 36	. . . . . . . . 9 ⊢ (∀𝑢 ¬ 𝑢 ∈ 𝑦 → (𝑧 = 𝑦 → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
102		elequ1 2151	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑧 → (𝑢 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦))
103	102	notbid 321	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑧 → (¬ 𝑢 ∈ 𝑦 ↔ ¬ 𝑧 ∈ 𝑦))
104	103	spvv 2020	. . . . . . . . . 10 ⊢ (∀𝑢 ¬ 𝑢 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑦)
105	104	pm2.21d 122	. . . . . . . . 9 ⊢ (∀𝑢 ¬ 𝑢 ∈ 𝑦 → (𝑧 ∈ 𝑦 → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
106	101, 105	jaod 873	. . . . . . . 8 ⊢ (∀𝑢 ¬ 𝑢 ∈ 𝑦 → ((𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
107	106	a1i 11	. . . . . . 7 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (∀𝑢 ¬ 𝑢 ∈ 𝑦 → ((𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))))
108	21, 78, 107	alrimdd 2250	. . . . . 6 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (∀𝑢 ¬ 𝑢 ∈ 𝑦 → ∀𝑧((𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))))
109	4, 108	eximd 2252	. . . . 5 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (∃𝑦∀𝑢 ¬ 𝑢 ∈ 𝑦 → ∃𝑦∀𝑧((𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))))
110	72, 109	mpi 21	. . . 4 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → ∃𝑦∀𝑧((𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
111		nfae 2462	. . . . 5 ⊢ Ⅎ𝑦∀𝑥 𝑥 = 𝑦
112		nfae 2462	. . . . . 6 ⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦
113		equequ2 2058	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))
114	113	sps 2221	. . . . . . . 8 ⊢ (∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))
115	114	orbi1d 930	. . . . . . 7 ⊢ (∀𝑥 𝑥 = 𝑦 → ((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) ↔ (𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦)))
116	115	imbi1d 344	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑦 → (((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)) ↔ ((𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))))
117	112, 116	albid 2258	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)) ↔ ∀𝑧((𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))))
118	111, 117	exbid 2259	. . . 4 ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)) ↔ ∃𝑦∀𝑧((𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))))
119	110, 118	imbitrrid 249	. . 3 ⊢ (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑧 → ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))))
120	71, 119	pm2.61d 181	. 2 ⊢ (∀𝑥 𝑥 = 𝑦 → ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
121		nfae 2462	. . . 4 ⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑧
122	87	a1d 26	. . . 4 ⊢ (∀𝑥 𝑥 = 𝑧 → ((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
123	121, 122	alrimi 2249	. . 3 ⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
124	123	19.8ad 2218	. 2 ⊢ (∀𝑥 𝑥 = 𝑧 → ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
125	61, 120, 124, 70	pm2.61iii 187	1 ⊢ ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103  ∀wal 1567  ∃wex 1811  Ⅎwnf 1815

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-13 2401  ax-sep 5248  ax-nul 5259  ax-reg 9586  ax-tco 37260

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-ex 1812  df-nf 1816

This theorem is used by: (None)