Theorem axtcond 36933

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 2402. (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 36929	. . . 4 ⊢ ∃𝑤∀𝑣((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤))
2		nfnae 2464	. . . . . 6 ⊢ Ⅎ𝑦 ¬ ∀𝑥 𝑥 = 𝑦
3		nfnae 2464	. . . . . 6 ⊢ Ⅎ𝑦 ¬ ∀𝑥 𝑥 = 𝑧
4		nfnae 2464	. . . . . 6 ⊢ Ⅎ𝑦 ¬ ∀𝑦 𝑦 = 𝑧
5	2, 3, 4	nf3an 1929	. . . . 5 ⊢ Ⅎ𝑦(¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧)
6		nfv 1942	. . . . . . . 8 ⊢ Ⅎ𝑦∀𝑣((𝑣 = 𝑡 ∨ 𝑣 ∈ 𝑤) → ∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑤))
7		equequ2 2054	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑥 → (𝑣 = 𝑡 ↔ 𝑣 = 𝑥))
8	7	orbi1d 929	. . . . . . . . . 10 ⊢ (𝑡 = 𝑥 → ((𝑣 = 𝑡 ∨ 𝑣 ∈ 𝑤) ↔ (𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤)))
9		elequ1 2148	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑥 → (𝑡 ∈ 𝑣 ↔ 𝑥 ∈ 𝑣))
10		elequ1 2148	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑥 → (𝑡 ∈ 𝑤 ↔ 𝑥 ∈ 𝑤))
11	9, 10	imbi12d 347	. . . . . . . . . . . 12 ⊢ (𝑡 = 𝑥 → ((𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑤) ↔ (𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)))
12	11	cbvalvw 2064	. . . . . . . . . . 11 ⊢ (∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑤) ↔ ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤))
13	12	a1i 11	. . . . . . . . . 10 ⊢ (𝑡 = 𝑥 → (∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑤) ↔ ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)))
14	8, 13	imbi12d 347	. . . . . . . . 9 ⊢ (𝑡 = 𝑥 → (((𝑣 = 𝑡 ∨ 𝑣 ∈ 𝑤) → ∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑤)) ↔ ((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤))))
15	14	albidv 1948	. . . . . . . 8 ⊢ (𝑡 = 𝑥 → (∀𝑣((𝑣 = 𝑡 ∨ 𝑣 ∈ 𝑤) → ∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑤)) ↔ ∀𝑣((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤))))
16	6, 15	dvelimnf 2483	. . . . . . 7 ⊢ (¬ ∀𝑦 𝑦 = 𝑥 → Ⅎ𝑦∀𝑣((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)))
17	16	naecoms 2459	. . . . . 6 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦∀𝑣((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)))
18	17	3ad2ant1 1149	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑦∀𝑣((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)))
19		nfnae 2464	. . . . . . . . 9 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦
20		nfnae 2464	. . . . . . . . 9 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑧
21		nfnae 2464	. . . . . . . . 9 ⊢ Ⅎ𝑧 ¬ ∀𝑦 𝑦 = 𝑧
22	19, 20, 21	nf3an 1929	. . . . . . . 8 ⊢ Ⅎ𝑧(¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧)
23		nfeqf2 2407	. . . . . . . . . 10 ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧 𝑤 = 𝑦)
24	23	naecoms 2459	. . . . . . . . 9 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧 𝑤 = 𝑦)
25	24	3ad2ant3 1151	. . . . . . . 8 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → Ⅎ𝑧 𝑤 = 𝑦)
26	22, 25	nfan1 2234	. . . . . . 7 ⊢ Ⅎ𝑧((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦)
27		simpl2 1209	. . . . . . . 8 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) → ¬ ∀𝑥 𝑥 = 𝑧)
28		nfv 1942	. . . . . . . . . 10 ⊢ Ⅎ𝑧((𝑣 = 𝑡 ∨ 𝑣 ∈ 𝑤) → ∀𝑡(𝑡 ∈ 𝑣 → 𝑡 ∈ 𝑤))
29	28, 14	dvelimnf 2483	. . . . . . . . 9 ⊢ (¬ ∀𝑧 𝑧 = 𝑥 → Ⅎ𝑧((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)))
30	29	naecoms 2459	. . . . . . . 8 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → Ⅎ𝑧((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)))
31	27, 30	syl 18	. . . . . . 7 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) → Ⅎ𝑧((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)))
32		equequ1 2053	. . . . . . . . . . . . 13 ⊢ (𝑣 = 𝑧 → (𝑣 = 𝑥 ↔ 𝑧 = 𝑥))
33	32	adantl 486	. . . . . . . . . . . 12 ⊢ ((𝑤 = 𝑦 ∧ 𝑣 = 𝑧) → (𝑣 = 𝑥 ↔ 𝑧 = 𝑥))
34		elequ12 2159	. . . . . . . . . . . . 13 ⊢ ((𝑣 = 𝑧 ∧ 𝑤 = 𝑦) → (𝑣 ∈ 𝑤 ↔ 𝑧 ∈ 𝑦))
35	34	ancoms 463	. . . . . . . . . . . 12 ⊢ ((𝑤 = 𝑦 ∧ 𝑣 = 𝑧) → (𝑣 ∈ 𝑤 ↔ 𝑧 ∈ 𝑦))
36	33, 35	orbi12d 931	. . . . . . . . . . 11 ⊢ ((𝑤 = 𝑦 ∧ 𝑣 = 𝑧) → ((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) ↔ (𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦)))
37	36	adantl 486	. . . . . . . . . 10 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ (𝑤 = 𝑦 ∧ 𝑣 = 𝑧)) → ((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) ↔ (𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦)))
38		nfnae 2464	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥 ¬ ∀𝑥 𝑥 = 𝑦
39		nfnae 2464	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥 ¬ ∀𝑥 𝑥 = 𝑧
40	38, 39	nfan 1927	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥(¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧)
41		nfeqf2 2407	. . . . . . . . . . . . . 14 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥 𝑤 = 𝑦)
42	41	adantr 485	. . . . . . . . . . . . 13 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑤 = 𝑦)
43		nfeqf2 2407	. . . . . . . . . . . . . 14 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥 𝑣 = 𝑧)
44	43	adantl 486	. . . . . . . . . . . . 13 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥 𝑣 = 𝑧)
45	42, 44	nfand 1925	. . . . . . . . . . . 12 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) → Ⅎ𝑥(𝑤 = 𝑦 ∧ 𝑣 = 𝑧))
46	40, 45	nfan1 2234	. . . . . . . . . . 11 ⊢ Ⅎ𝑥((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ (𝑤 = 𝑦 ∧ 𝑣 = 𝑧))
47		elequ2 2156	. . . . . . . . . . . . . 14 ⊢ (𝑣 = 𝑧 → (𝑥 ∈ 𝑣 ↔ 𝑥 ∈ 𝑧))
48	47	adantl 486	. . . . . . . . . . . . 13 ⊢ ((𝑤 = 𝑦 ∧ 𝑣 = 𝑧) → (𝑥 ∈ 𝑣 ↔ 𝑥 ∈ 𝑧))
49		elequ2 2156	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑦 → (𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑦))
50	49	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝑤 = 𝑦 ∧ 𝑣 = 𝑧) → (𝑥 ∈ 𝑤 ↔ 𝑥 ∈ 𝑦))
51	48, 50	imbi12d 347	. . . . . . . . . . . 12 ⊢ ((𝑤 = 𝑦 ∧ 𝑣 = 𝑧) → ((𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤) ↔ (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
52	51	adantl 486	. . . . . . . . . . 11 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ (𝑤 = 𝑦 ∧ 𝑣 = 𝑧)) → ((𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤) ↔ (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
53	46, 52	albid 2256	. . . . . . . . . 10 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ (𝑤 = 𝑦 ∧ 𝑣 = 𝑧)) → (∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤) ↔ ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
54	37, 53	imbi12d 347	. . . . . . . . 9 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ (𝑤 = 𝑦 ∧ 𝑣 = 𝑧)) → (((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)) ↔ ((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))))
55	54	expr 461	. . . . . . . 8 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧) ∧ 𝑤 = 𝑦) → (𝑣 = 𝑧 → (((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)) ↔ ((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))))
56	55	3adantl3 1185	. . . . . . 7 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) → (𝑣 = 𝑧 → (((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)) ↔ ((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))))
57	26, 31, 56	cbvaldw 2368	. . . . . 6 ⊢ (((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) ∧ 𝑤 = 𝑦) → (∀𝑣((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)) ↔ ∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))))
58	57	ex 417	. . . . 5 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (𝑤 = 𝑦 → (∀𝑣((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)) ↔ ∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))))
59	5, 18, 58	cbvexdw 2369	. . . 4 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → (∃𝑤∀𝑣((𝑣 = 𝑥 ∨ 𝑣 ∈ 𝑤) → ∀𝑥(𝑥 ∈ 𝑣 → 𝑥 ∈ 𝑤)) ↔ ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))))
60	1, 59	mpbii 236	. . 3 ⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∧ ¬ ∀𝑥 𝑥 = 𝑧 ∧ ¬ ∀𝑦 𝑦 = 𝑧) → ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
61	60	3exp 1135	. 2 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑥 𝑥 = 𝑧 → (¬ ∀𝑦 𝑦 = 𝑧 → ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))))
62		nfae 2463	. . . . . 6 ⊢ Ⅎ𝑧∀𝑦 𝑦 = 𝑧
63		nfae 2463	. . . . . . . 8 ⊢ Ⅎ𝑥∀𝑦 𝑦 = 𝑧
64		elequ2 2156	. . . . . . . . . 10 ⊢ (𝑦 = 𝑧 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧))
65	64	sps 2219	. . . . . . . . 9 ⊢ (∀𝑦 𝑦 = 𝑧 → (𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝑧))
66	65	biimprd 251	. . . . . . . 8 ⊢ (∀𝑦 𝑦 = 𝑧 → (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))
67	63, 66	alrimi 2247	. . . . . . 7 ⊢ (∀𝑦 𝑦 = 𝑧 → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))
68	67	a1d 26	. . . . . 6 ⊢ (∀𝑦 𝑦 = 𝑧 → ((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
69	62, 68	alrimi 2247	. . . . 5 ⊢ (∀𝑦 𝑦 = 𝑧 → ∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
70	69	19.8ad 2216	. . . 4 ⊢ (∀𝑦 𝑦 = 𝑧 → ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
71	70	a1i 11	. . 3 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑦 𝑦 = 𝑧 → ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))))
72		ax-nul 5268	. . . . 5 ⊢ ∃𝑦∀𝑢 ¬ 𝑢 ∈ 𝑦
73		nfv 1942	. . . . . . . . 9 ⊢ Ⅎ𝑧∀𝑢 ¬ 𝑢 ∈ 𝑡
74		elequ2 2156	. . . . . . . . . . 11 ⊢ (𝑡 = 𝑦 → (𝑢 ∈ 𝑡 ↔ 𝑢 ∈ 𝑦))
75	74	notbid 321	. . . . . . . . . 10 ⊢ (𝑡 = 𝑦 → (¬ 𝑢 ∈ 𝑡 ↔ ¬ 𝑢 ∈ 𝑦))
76	75	albidv 1948	. . . . . . . . 9 ⊢ (𝑡 = 𝑦 → (∀𝑢 ¬ 𝑢 ∈ 𝑡 ↔ ∀𝑢 ¬ 𝑢 ∈ 𝑦))
77	73, 76	dvelimnf 2483	. . . . . . . 8 ⊢ (¬ ∀𝑧 𝑧 = 𝑦 → Ⅎ𝑧∀𝑢 ¬ 𝑢 ∈ 𝑦)
78	77	naecoms 2459	. . . . . . 7 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → Ⅎ𝑧∀𝑢 ¬ 𝑢 ∈ 𝑦)
79		elequ2 2156	. . . . . . . . . . . . 13 ⊢ (𝑧 = 𝑦 → (𝑢 ∈ 𝑧 ↔ 𝑢 ∈ 𝑦))
80	79	notbid 321	. . . . . . . . . . . 12 ⊢ (𝑧 = 𝑦 → (¬ 𝑢 ∈ 𝑧 ↔ ¬ 𝑢 ∈ 𝑦))
81	80	albidv 1948	. . . . . . . . . . 11 ⊢ (𝑧 = 𝑦 → (∀𝑢 ¬ 𝑢 ∈ 𝑧 ↔ ∀𝑢 ¬ 𝑢 ∈ 𝑦))
82	81	biimprcd 253	. . . . . . . . . 10 ⊢ (∀𝑢 ¬ 𝑢 ∈ 𝑦 → (𝑧 = 𝑦 → ∀𝑢 ¬ 𝑢 ∈ 𝑧))
83		elirrv 9558	. . . . . . . . . . . . . . 15 ⊢ ¬ 𝑥 ∈ 𝑥
84		elequ2 2156	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝑥 ↔ 𝑥 ∈ 𝑧))
85	83, 84	mtbii 329	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑧 → ¬ 𝑥 ∈ 𝑧)
86	85	pm2.21d 122	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))
87	86	alimi 1839	. . . . . . . . . . . 12 ⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))
88	87	a1d 26	. . . . . . . . . . 11 ⊢ (∀𝑥 𝑥 = 𝑧 → (∀𝑢 ¬ 𝑢 ∈ 𝑧 → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
89		nfv 1942	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥∀𝑢 ¬ 𝑢 ∈ 𝑡
90		elequ2 2156	. . . . . . . . . . . . . . 15 ⊢ (𝑡 = 𝑧 → (𝑢 ∈ 𝑡 ↔ 𝑢 ∈ 𝑧))
91	90	notbid 321	. . . . . . . . . . . . . 14 ⊢ (𝑡 = 𝑧 → (¬ 𝑢 ∈ 𝑡 ↔ ¬ 𝑢 ∈ 𝑧))
92	91	albidv 1948	. . . . . . . . . . . . 13 ⊢ (𝑡 = 𝑧 → (∀𝑢 ¬ 𝑢 ∈ 𝑡 ↔ ∀𝑢 ¬ 𝑢 ∈ 𝑧))
93	89, 92	dvelimnf 2483	. . . . . . . . . . . 12 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥∀𝑢 ¬ 𝑢 ∈ 𝑧)
94		elequ1 2148	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑥 → (𝑢 ∈ 𝑧 ↔ 𝑥 ∈ 𝑧))
95	94	notbid 321	. . . . . . . . . . . . . . 15 ⊢ (𝑢 = 𝑥 → (¬ 𝑢 ∈ 𝑧 ↔ ¬ 𝑥 ∈ 𝑧))
96	95	spvv 2016	. . . . . . . . . . . . . 14 ⊢ (∀𝑢 ¬ 𝑢 ∈ 𝑧 → ¬ 𝑥 ∈ 𝑧)
97	96	pm2.21d 122	. . . . . . . . . . . . 13 ⊢ (∀𝑢 ¬ 𝑢 ∈ 𝑧 → (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))
98	97	a1i 11	. . . . . . . . . . . 12 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → (∀𝑢 ¬ 𝑢 ∈ 𝑧 → (𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
99	39, 93, 98	alrimdd 2248	. . . . . . . . . . 11 ⊢ (¬ ∀𝑥 𝑥 = 𝑧 → (∀𝑢 ¬ 𝑢 ∈ 𝑧 → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
100	88, 99	pm2.61i 184	. . . . . . . . . 10 ⊢ (∀𝑢 ¬ 𝑢 ∈ 𝑧 → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))
101	82, 100	syl6 36	. . . . . . . . 9 ⊢ (∀𝑢 ¬ 𝑢 ∈ 𝑦 → (𝑧 = 𝑦 → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
102		elequ1 2148	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑧 → (𝑢 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦))
103	102	notbid 321	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑧 → (¬ 𝑢 ∈ 𝑦 ↔ ¬ 𝑧 ∈ 𝑦))
104	103	spvv 2016	. . . . . . . . . 10 ⊢ (∀𝑢 ¬ 𝑢 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑦)
105	104	pm2.21d 122	. . . . . . . . 9 ⊢ (∀𝑢 ¬ 𝑢 ∈ 𝑦 → (𝑧 ∈ 𝑦 → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
106	101, 105	jaod 872	. . . . . . . 8 ⊢ (∀𝑢 ¬ 𝑢 ∈ 𝑦 → ((𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
107	106	a1i 11	. . . . . . 7 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (∀𝑢 ¬ 𝑢 ∈ 𝑦 → ((𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))))
108	21, 78, 107	alrimdd 2248	. . . . . 6 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (∀𝑢 ¬ 𝑢 ∈ 𝑦 → ∀𝑧((𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))))
109	4, 108	eximd 2250	. . . . 5 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → (∃𝑦∀𝑢 ¬ 𝑢 ∈ 𝑦 → ∃𝑦∀𝑧((𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))))
110	72, 109	mpi 21	. . . 4 ⊢ (¬ ∀𝑦 𝑦 = 𝑧 → ∃𝑦∀𝑧((𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
111		nfae 2463	. . . . 5 ⊢ Ⅎ𝑦∀𝑥 𝑥 = 𝑦
112		nfae 2463	. . . . . 6 ⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑦
113		equequ2 2054	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))
114	113	sps 2219	. . . . . . . 8 ⊢ (∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑥 ↔ 𝑧 = 𝑦))
115	114	orbi1d 929	. . . . . . 7 ⊢ (∀𝑥 𝑥 = 𝑦 → ((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) ↔ (𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦)))
116	115	imbi1d 344	. . . . . 6 ⊢ (∀𝑥 𝑥 = 𝑦 → (((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)) ↔ ((𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))))
117	112, 116	albid 2256	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑦 → (∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)) ↔ ∀𝑧((𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))))
118	111, 117	exbid 2257	. . . 4 ⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)) ↔ ∃𝑦∀𝑧((𝑧 = 𝑦 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))))
119	110, 118	imbitrrid 249	. . 3 ⊢ (∀𝑥 𝑥 = 𝑦 → (¬ ∀𝑦 𝑦 = 𝑧 → ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))))
120	71, 119	pm2.61d 181	. 2 ⊢ (∀𝑥 𝑥 = 𝑦 → ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
121		nfae 2463	. . . 4 ⊢ Ⅎ𝑧∀𝑥 𝑥 = 𝑧
122	87	a1d 26	. . . 4 ⊢ (∀𝑥 𝑥 = 𝑧 → ((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
123	121, 122	alrimi 2247	. . 3 ⊢ (∀𝑥 𝑥 = 𝑧 → ∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
124	123	19.8ad 2216	. 2 ⊢ (∀𝑥 𝑥 = 𝑧 → ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦)))
125	61, 120, 124, 70	pm2.61iii 187	1 ⊢ ∃𝑦∀𝑧((𝑧 = 𝑥 ∨ 𝑧 ∈ 𝑦) → ∀𝑥(𝑥 ∈ 𝑧 → 𝑥 ∈ 𝑦))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 860   ∧ w3a 1101  ∀wal 1566  ∃wex 1807  Ⅎwnf 1811

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-13 2402  ax-sep 5256  ax-nul 5268  ax-reg 9553  ax-tco 36927

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-ex 1808  df-nf 1812

This theorem is referenced by: (None)