Theorem mirimanofffr 36628

Description: Relative version of mirimanofff 36629 (which corresponds to the case 𝑉 = V). (Contributed by Adrian Ducourtial, 28-Oct-2026.)

Hypothesis

Ref	Expression
mirimanofffr.1	⊢ 𝑀 = {𝑥 ∈ 𝑉 ∣ ∀𝑦(𝑥 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅)}

Assertion

Ref	Expression
mirimanofffr	⊢ 𝑀 ∉ 𝑉

Distinct variable groups:   𝑥,𝑉,𝑧   𝑥,𝑀,𝑦,𝑧

Allowed substitution hint:   𝑉(𝑦)

Proof of Theorem mirimanofffr

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

Step	Hyp	Ref	Expression
1		pm3.24 408	. . . . 5 ⊢ ¬ (𝑣 ∈ 𝑀 ∧ ¬ 𝑣 ∈ 𝑀)
2		ancom 466	. . . . 5 ⊢ ((𝑣 ∈ 𝑀 ∧ ¬ 𝑣 ∈ 𝑀) ↔ (¬ 𝑣 ∈ 𝑀 ∧ 𝑣 ∈ 𝑀))
3	1, 2	mtbi 325	. . . 4 ⊢ ¬ (¬ 𝑣 ∈ 𝑀 ∧ 𝑣 ∈ 𝑀)
4	3	nex 1833	. . 3 ⊢ ¬ ∃𝑣(¬ 𝑣 ∈ 𝑀 ∧ 𝑣 ∈ 𝑀)
5		pm2.24 125	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ 𝑉 → (¬ 𝑀 ∈ 𝑉 → ¬ ∀𝑦(𝑀 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅)))
6		idd 25	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ 𝑉 → (¬ ∀𝑦(𝑀 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅) → ¬ ∀𝑦(𝑀 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅)))
7		snexg 5402	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 ∈ 𝑉 → {𝑀} ∈ V)
8		snidg 4621	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑀 ∈ 𝑉 → 𝑀 ∈ {𝑀})
9		eleq1 2852	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑀 → (𝑥 ∈ 𝑦 ↔ 𝑀 ∈ 𝑦))
10	9	imbi1d 344	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑥 = 𝑀 → ((𝑥 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅) ↔ (𝑀 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅)))
11	10	albidv 1955	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑥 = 𝑀 → (∀𝑦(𝑥 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅) ↔ ∀𝑦(𝑀 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅)))
12		mirimanofffr.1	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ 𝑀 = {𝑥 ∈ 𝑉 ∣ ∀𝑦(𝑥 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅)}
13	11, 12	elrab2 3652	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀 ∈ 𝑀 ↔ (𝑀 ∈ 𝑉 ∧ ∀𝑦(𝑀 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅)))
14	13	simprbi 503	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ 𝑀 → ∀𝑦(𝑀 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅))
15		eleq2 2853	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = {𝑀} → (𝑀 ∈ 𝑦 ↔ 𝑀 ∈ {𝑀}))
16		ineq2 4114	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = {𝑀} → (𝑧 ∩ 𝑦) = (𝑧 ∩ {𝑀}))
17	16	eqeq1d 2765	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑦 = {𝑀} → ((𝑧 ∩ 𝑦) = ∅ ↔ (𝑧 ∩ {𝑀}) = ∅))
18	17	rexeqbi1dv 3334	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑦 = {𝑀} → (∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅ ↔ ∃𝑧 ∈ {𝑀} (𝑧 ∩ {𝑀}) = ∅))
19	15, 18	imbi12d 347	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = {𝑀} → ((𝑀 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅) ↔ (𝑀 ∈ {𝑀} → ∃𝑧 ∈ {𝑀} (𝑧 ∩ {𝑀}) = ∅)))
20	19	spcgv 3554	. . . . . . . . . . . . . . . . . . . 20 ⊢ ({𝑀} ∈ V → (∀𝑦(𝑀 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅) → (𝑀 ∈ {𝑀} → ∃𝑧 ∈ {𝑀} (𝑧 ∩ {𝑀}) = ∅)))
21	14, 20	syl5 35	. . . . . . . . . . . . . . . . . . 19 ⊢ ({𝑀} ∈ V → (𝑀 ∈ 𝑀 → (𝑀 ∈ {𝑀} → ∃𝑧 ∈ {𝑀} (𝑧 ∩ {𝑀}) = ∅)))
22	21	com23 87	. . . . . . . . . . . . . . . . . 18 ⊢ ({𝑀} ∈ V → (𝑀 ∈ {𝑀} → (𝑀 ∈ 𝑀 → ∃𝑧 ∈ {𝑀} (𝑧 ∩ {𝑀}) = ∅)))
23	7, 8, 22	sylc 66	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ 𝑉 → (𝑀 ∈ 𝑀 → ∃𝑧 ∈ {𝑀} (𝑧 ∩ {𝑀}) = ∅))
24		elsn2g 4625	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑀 ∈ 𝑉 → (𝑧 ∈ {𝑀} ↔ 𝑧 = 𝑀))
25		ineq1 4113	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑧 = 𝑀 → (𝑧 ∩ {𝑀}) = (𝑀 ∩ {𝑀}))
26	25	eqeq1d 2765	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑧 = 𝑀 → ((𝑧 ∩ {𝑀}) = ∅ ↔ (𝑀 ∩ {𝑀}) = ∅))
27	24, 26	biimtrdi 256	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀 ∈ 𝑉 → (𝑧 ∈ {𝑀} → ((𝑧 ∩ {𝑀}) = ∅ ↔ (𝑀 ∩ {𝑀}) = ∅)))
28	27	imp 412	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝑧 ∈ {𝑀}) → ((𝑧 ∩ {𝑀}) = ∅ ↔ (𝑀 ∩ {𝑀}) = ∅))
29		disjr 4407	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑀 ∩ {𝑀}) = ∅ ↔ ∀𝑤 ∈ {𝑀} ¬ 𝑤 ∈ 𝑀)
30	28, 29	bitrdi 290	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝑧 ∈ {𝑀}) → ((𝑧 ∩ {𝑀}) = ∅ ↔ ∀𝑤 ∈ {𝑀} ¬ 𝑤 ∈ 𝑀))
31		eleq1 2852	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 = 𝑀 → (𝑤 ∈ 𝑀 ↔ 𝑀 ∈ 𝑀))
32	31	notbid 321	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 = 𝑀 → (¬ 𝑤 ∈ 𝑀 ↔ ¬ 𝑀 ∈ 𝑀))
33	32	rspcv 3576	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑀 ∈ {𝑀} → (∀𝑤 ∈ {𝑀} ¬ 𝑤 ∈ 𝑀 → ¬ 𝑀 ∈ 𝑀))
34	8, 33	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑀 ∈ 𝑉 → (∀𝑤 ∈ {𝑀} ¬ 𝑤 ∈ 𝑀 → ¬ 𝑀 ∈ 𝑀))
35	34	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝑧 ∈ {𝑀}) → (∀𝑤 ∈ {𝑀} ¬ 𝑤 ∈ 𝑀 → ¬ 𝑀 ∈ 𝑀))
36	30, 35	sylbid 243	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑀 ∈ 𝑉 ∧ 𝑧 ∈ {𝑀}) → ((𝑧 ∩ {𝑀}) = ∅ → ¬ 𝑀 ∈ 𝑀))
37	36	rexlimdva 3167	. . . . . . . . . . . . . . . . 17 ⊢ (𝑀 ∈ 𝑉 → (∃𝑧 ∈ {𝑀} (𝑧 ∩ {𝑀}) = ∅ → ¬ 𝑀 ∈ 𝑀))
38	23, 37	syld 48	. . . . . . . . . . . . . . . 16 ⊢ (𝑀 ∈ 𝑉 → (𝑀 ∈ 𝑀 → ¬ 𝑀 ∈ 𝑀))
39	38	pm2.01d 192	. . . . . . . . . . . . . . 15 ⊢ (𝑀 ∈ 𝑉 → ¬ 𝑀 ∈ 𝑀)
40	13	notbii 323	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑀 ∈ 𝑀 ↔ ¬ (𝑀 ∈ 𝑉 ∧ ∀𝑦(𝑀 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅)))
41	39, 40	sylib 221	. . . . . . . . . . . . . 14 ⊢ (𝑀 ∈ 𝑉 → ¬ (𝑀 ∈ 𝑉 ∧ ∀𝑦(𝑀 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅)))
42		ianor 997	. . . . . . . . . . . . . 14 ⊢ (¬ (𝑀 ∈ 𝑉 ∧ ∀𝑦(𝑀 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅)) ↔ (¬ 𝑀 ∈ 𝑉 ∨ ¬ ∀𝑦(𝑀 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅)))
43	41, 42	sylib 221	. . . . . . . . . . . . 13 ⊢ (𝑀 ∈ 𝑉 → (¬ 𝑀 ∈ 𝑉 ∨ ¬ ∀𝑦(𝑀 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅)))
44	5, 6, 43	mpjaod 874	. . . . . . . . . . . 12 ⊢ (𝑀 ∈ 𝑉 → ¬ ∀𝑦(𝑀 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅))
45		exanali 1892	. . . . . . . . . . . 12 ⊢ (∃𝑦(𝑀 ∈ 𝑦 ∧ ¬ ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅) ↔ ¬ ∀𝑦(𝑀 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅))
46	44, 45	sylibr 237	. . . . . . . . . . 11 ⊢ (𝑀 ∈ 𝑉 → ∃𝑦(𝑀 ∈ 𝑦 ∧ ¬ ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅))
47		df-rex 3091	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅ ↔ ∃𝑧(𝑧 ∈ 𝑦 ∧ (𝑧 ∩ 𝑦) = ∅))
48	47	notbii 323	. . . . . . . . . . . . . . 15 ⊢ (¬ ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅ ↔ ¬ ∃𝑧(𝑧 ∈ 𝑦 ∧ (𝑧 ∩ 𝑦) = ∅))
49		alnex 1814	. . . . . . . . . . . . . . 15 ⊢ (∀𝑧 ¬ (𝑧 ∈ 𝑦 ∧ (𝑧 ∩ 𝑦) = ∅) ↔ ¬ ∃𝑧(𝑧 ∈ 𝑦 ∧ (𝑧 ∩ 𝑦) = ∅))
50		ianor 997	. . . . . . . . . . . . . . . . 17 ⊢ (¬ (𝑧 ∈ 𝑦 ∧ (𝑧 ∩ 𝑦) = ∅) ↔ (¬ 𝑧 ∈ 𝑦 ∨ ¬ (𝑧 ∩ 𝑦) = ∅))
51		imor 867	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑧 ∈ 𝑦 → ¬ (𝑧 ∩ 𝑦) = ∅) ↔ (¬ 𝑧 ∈ 𝑦 ∨ ¬ (𝑧 ∩ 𝑦) = ∅))
52	50, 51	bitr4i 281	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝑧 ∈ 𝑦 ∧ (𝑧 ∩ 𝑦) = ∅) ↔ (𝑧 ∈ 𝑦 → ¬ (𝑧 ∩ 𝑦) = ∅))
53	52	albii 1852	. . . . . . . . . . . . . . 15 ⊢ (∀𝑧 ¬ (𝑧 ∈ 𝑦 ∧ (𝑧 ∩ 𝑦) = ∅) ↔ ∀𝑧(𝑧 ∈ 𝑦 → ¬ (𝑧 ∩ 𝑦) = ∅))
54	48, 49, 53	3bitr2i 302	. . . . . . . . . . . . . 14 ⊢ (¬ ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅ ↔ ∀𝑧(𝑧 ∈ 𝑦 → ¬ (𝑧 ∩ 𝑦) = ∅))
55		df-ral 3081	. . . . . . . . . . . . . 14 ⊢ (∀𝑧 ∈ 𝑦 ¬ (𝑧 ∩ 𝑦) = ∅ ↔ ∀𝑧(𝑧 ∈ 𝑦 → ¬ (𝑧 ∩ 𝑦) = ∅))
56		df-ral 3081	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑤 ∈ 𝑦 ¬ 𝑤 ∈ 𝑧 ↔ ∀𝑤(𝑤 ∈ 𝑦 → ¬ 𝑤 ∈ 𝑧))
57	56	notbii 323	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ ∀𝑤 ∈ 𝑦 ¬ 𝑤 ∈ 𝑧 ↔ ¬ ∀𝑤(𝑤 ∈ 𝑦 → ¬ 𝑤 ∈ 𝑧))
58		disjr 4407	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑧 ∩ 𝑦) = ∅ ↔ ∀𝑤 ∈ 𝑦 ¬ 𝑤 ∈ 𝑧)
59	57, 58	xchnxbir 336	. . . . . . . . . . . . . . . . 17 ⊢ (¬ (𝑧 ∩ 𝑦) = ∅ ↔ ¬ ∀𝑤(𝑤 ∈ 𝑦 → ¬ 𝑤 ∈ 𝑧))
60		exnal 1860	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑤 ¬ (𝑤 ∈ 𝑦 → ¬ 𝑤 ∈ 𝑧) ↔ ¬ ∀𝑤(𝑤 ∈ 𝑦 → ¬ 𝑤 ∈ 𝑧))
61		pm4.63 403	. . . . . . . . . . . . . . . . . 18 ⊢ (¬ (𝑤 ∈ 𝑦 → ¬ 𝑤 ∈ 𝑧) ↔ (𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑧))
62	61	exbii 1881	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑤 ¬ (𝑤 ∈ 𝑦 → ¬ 𝑤 ∈ 𝑧) ↔ ∃𝑤(𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑧))
63	59, 60, 62	3bitr2i 302	. . . . . . . . . . . . . . . 16 ⊢ (¬ (𝑧 ∩ 𝑦) = ∅ ↔ ∃𝑤(𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑧))
64		df-rex 3091	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧 ↔ ∃𝑤(𝑤 ∈ 𝑦 ∧ 𝑤 ∈ 𝑧))
65	63, 64	bitr4i 281	. . . . . . . . . . . . . . 15 ⊢ (¬ (𝑧 ∩ 𝑦) = ∅ ↔ ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧)
66	65	ralbii 3112	. . . . . . . . . . . . . 14 ⊢ (∀𝑧 ∈ 𝑦 ¬ (𝑧 ∩ 𝑦) = ∅ ↔ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧)
67	54, 55, 66	3bitr2i 302	. . . . . . . . . . . . 13 ⊢ (¬ ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅ ↔ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧)
68	67	anbi2i 635	. . . . . . . . . . . 12 ⊢ ((𝑀 ∈ 𝑦 ∧ ¬ ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅) ↔ (𝑀 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧))
69	68	exbii 1881	. . . . . . . . . . 11 ⊢ (∃𝑦(𝑀 ∈ 𝑦 ∧ ¬ ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅) ↔ ∃𝑦(𝑀 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧))
70	46, 69	sylib 221	. . . . . . . . . 10 ⊢ (𝑀 ∈ 𝑉 → ∃𝑦(𝑀 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧))
71		eleq2w2 2759	. . . . . . . . . . . . . . 15 ⊢ (𝑧 = 𝑀 → (𝑤 ∈ 𝑧 ↔ 𝑤 ∈ 𝑀))
72	71	rexbidv 3190	. . . . . . . . . . . . . 14 ⊢ (𝑧 = 𝑀 → (∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧 ↔ ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑀))
73	72	rspcva 3578	. . . . . . . . . . . . 13 ⊢ ((𝑀 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧) → ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑀)
74	73	anim2i 629	. . . . . . . . . . . 12 ⊢ ((∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧 ∧ (𝑀 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧)) → (∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧 ∧ ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑀))
75	74	anabss7 686	. . . . . . . . . . 11 ⊢ ((𝑀 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧) → (∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧 ∧ ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑀))
76	75	eximi 1868	. . . . . . . . . 10 ⊢ (∃𝑦(𝑀 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧) → ∃𝑦(∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧 ∧ ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑀))
77	70, 76	syl 18	. . . . . . . . 9 ⊢ (𝑀 ∈ 𝑉 → ∃𝑦(∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧 ∧ ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑀))
78		eleq1w 2847	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑣 → (𝑤 ∈ 𝑀 ↔ 𝑣 ∈ 𝑀))
79	78	cbvrexvw 3245	. . . . . . . . . . 11 ⊢ (∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑀 ↔ ∃𝑣 ∈ 𝑦 𝑣 ∈ 𝑀)
80	79	anbi2i 635	. . . . . . . . . 10 ⊢ ((∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧 ∧ ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑀) ↔ (∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ 𝑦 𝑣 ∈ 𝑀))
81	80	exbii 1881	. . . . . . . . 9 ⊢ (∃𝑦(∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧 ∧ ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑀) ↔ ∃𝑦(∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ 𝑦 𝑣 ∈ 𝑀))
82	77, 81	sylib 221	. . . . . . . 8 ⊢ (𝑀 ∈ 𝑉 → ∃𝑦(∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ 𝑦 𝑣 ∈ 𝑀))
83		r19.41v 3196	. . . . . . . . . 10 ⊢ (∃𝑣 ∈ 𝑦 (𝑣 ∈ 𝑀 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧) ↔ (∃𝑣 ∈ 𝑦 𝑣 ∈ 𝑀 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧))
84	83	biancomi 468	. . . . . . . . 9 ⊢ (∃𝑣 ∈ 𝑦 (𝑣 ∈ 𝑀 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧) ↔ (∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ 𝑦 𝑣 ∈ 𝑀))
85	84	exbii 1881	. . . . . . . 8 ⊢ (∃𝑦∃𝑣 ∈ 𝑦 (𝑣 ∈ 𝑀 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧) ↔ ∃𝑦(∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧 ∧ ∃𝑣 ∈ 𝑦 𝑣 ∈ 𝑀))
86	82, 85	sylibr 237	. . . . . . 7 ⊢ (𝑀 ∈ 𝑉 → ∃𝑦∃𝑣 ∈ 𝑦 (𝑣 ∈ 𝑀 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧))
87		df-rex 3091	. . . . . . . . 9 ⊢ (∃𝑣 ∈ 𝑦 (𝑣 ∈ 𝑀 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧) ↔ ∃𝑣(𝑣 ∈ 𝑦 ∧ (𝑣 ∈ 𝑀 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧)))
88		3anass 1111	. . . . . . . . . 10 ⊢ ((𝑣 ∈ 𝑦 ∧ 𝑣 ∈ 𝑀 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧) ↔ (𝑣 ∈ 𝑦 ∧ (𝑣 ∈ 𝑀 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧)))
89	88	exbii 1881	. . . . . . . . 9 ⊢ (∃𝑣(𝑣 ∈ 𝑦 ∧ 𝑣 ∈ 𝑀 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧) ↔ ∃𝑣(𝑣 ∈ 𝑦 ∧ (𝑣 ∈ 𝑀 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧)))
90	87, 89	bitr4i 281	. . . . . . . 8 ⊢ (∃𝑣 ∈ 𝑦 (𝑣 ∈ 𝑀 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧) ↔ ∃𝑣(𝑣 ∈ 𝑦 ∧ 𝑣 ∈ 𝑀 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧))
91	90	exbii 1881	. . . . . . 7 ⊢ (∃𝑦∃𝑣 ∈ 𝑦 (𝑣 ∈ 𝑀 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧) ↔ ∃𝑦∃𝑣(𝑣 ∈ 𝑦 ∧ 𝑣 ∈ 𝑀 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧))
92	86, 91	sylib 221	. . . . . 6 ⊢ (𝑀 ∈ 𝑉 → ∃𝑦∃𝑣(𝑣 ∈ 𝑦 ∧ 𝑣 ∈ 𝑀 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧))
93		excom 2202	. . . . . 6 ⊢ (∃𝑦∃𝑣(𝑣 ∈ 𝑦 ∧ 𝑣 ∈ 𝑀 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧) ↔ ∃𝑣∃𝑦(𝑣 ∈ 𝑦 ∧ 𝑣 ∈ 𝑀 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧))
94	92, 93	sylib 221	. . . . 5 ⊢ (𝑀 ∈ 𝑉 → ∃𝑣∃𝑦(𝑣 ∈ 𝑦 ∧ 𝑣 ∈ 𝑀 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧))
95		3ancomb 1116	. . . . . 6 ⊢ ((𝑣 ∈ 𝑦 ∧ 𝑣 ∈ 𝑀 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧) ↔ (𝑣 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧 ∧ 𝑣 ∈ 𝑀))
96	95	2exbii 1882	. . . . 5 ⊢ (∃𝑣∃𝑦(𝑣 ∈ 𝑦 ∧ 𝑣 ∈ 𝑀 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧) ↔ ∃𝑣∃𝑦(𝑣 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧 ∧ 𝑣 ∈ 𝑀))
97	94, 96	sylib 221	. . . 4 ⊢ (𝑀 ∈ 𝑉 → ∃𝑣∃𝑦(𝑣 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧 ∧ 𝑣 ∈ 𝑀))
98		df-3an 1105	. . . . . . 7 ⊢ ((𝑣 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧 ∧ 𝑣 ∈ 𝑀) ↔ ((𝑣 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧) ∧ 𝑣 ∈ 𝑀))
99	98	exbii 1881	. . . . . 6 ⊢ (∃𝑦(𝑣 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧 ∧ 𝑣 ∈ 𝑀) ↔ ∃𝑦((𝑣 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧) ∧ 𝑣 ∈ 𝑀))
100		19.41v 1984	. . . . . . 7 ⊢ (∃𝑦((𝑣 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧) ∧ 𝑣 ∈ 𝑀) ↔ (∃𝑦(𝑣 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧) ∧ 𝑣 ∈ 𝑀))
101		pm4.61 410	. . . . . . . . . . . . . 14 ⊢ (¬ (𝑣 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅) ↔ (𝑣 ∈ 𝑦 ∧ ¬ ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅))
102	101	exbii 1881	. . . . . . . . . . . . 13 ⊢ (∃𝑦 ¬ (𝑣 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅) ↔ ∃𝑦(𝑣 ∈ 𝑦 ∧ ¬ ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅))
103		exnal 1860	. . . . . . . . . . . . 13 ⊢ (∃𝑦 ¬ (𝑣 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅) ↔ ¬ ∀𝑦(𝑣 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅))
104	48	anbi2i 635	. . . . . . . . . . . . . 14 ⊢ ((𝑣 ∈ 𝑦 ∧ ¬ ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅) ↔ (𝑣 ∈ 𝑦 ∧ ¬ ∃𝑧(𝑧 ∈ 𝑦 ∧ (𝑧 ∩ 𝑦) = ∅)))
105	104	exbii 1881	. . . . . . . . . . . . 13 ⊢ (∃𝑦(𝑣 ∈ 𝑦 ∧ ¬ ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅) ↔ ∃𝑦(𝑣 ∈ 𝑦 ∧ ¬ ∃𝑧(𝑧 ∈ 𝑦 ∧ (𝑧 ∩ 𝑦) = ∅)))
106	102, 103, 105	3bitr3i 304	. . . . . . . . . . . 12 ⊢ (¬ ∀𝑦(𝑣 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅) ↔ ∃𝑦(𝑣 ∈ 𝑦 ∧ ¬ ∃𝑧(𝑧 ∈ 𝑦 ∧ (𝑧 ∩ 𝑦) = ∅)))
107	49	anbi2i 635	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ 𝑦 ∧ ∀𝑧 ¬ (𝑧 ∈ 𝑦 ∧ (𝑧 ∩ 𝑦) = ∅)) ↔ (𝑣 ∈ 𝑦 ∧ ¬ ∃𝑧(𝑧 ∈ 𝑦 ∧ (𝑧 ∩ 𝑦) = ∅)))
108	107	exbii 1881	. . . . . . . . . . . 12 ⊢ (∃𝑦(𝑣 ∈ 𝑦 ∧ ∀𝑧 ¬ (𝑧 ∈ 𝑦 ∧ (𝑧 ∩ 𝑦) = ∅)) ↔ ∃𝑦(𝑣 ∈ 𝑦 ∧ ¬ ∃𝑧(𝑧 ∈ 𝑦 ∧ (𝑧 ∩ 𝑦) = ∅)))
109	50	albii 1852	. . . . . . . . . . . . . 14 ⊢ (∀𝑧 ¬ (𝑧 ∈ 𝑦 ∧ (𝑧 ∩ 𝑦) = ∅) ↔ ∀𝑧(¬ 𝑧 ∈ 𝑦 ∨ ¬ (𝑧 ∩ 𝑦) = ∅))
110	109	anbi2i 635	. . . . . . . . . . . . 13 ⊢ ((𝑣 ∈ 𝑦 ∧ ∀𝑧 ¬ (𝑧 ∈ 𝑦 ∧ (𝑧 ∩ 𝑦) = ∅)) ↔ (𝑣 ∈ 𝑦 ∧ ∀𝑧(¬ 𝑧 ∈ 𝑦 ∨ ¬ (𝑧 ∩ 𝑦) = ∅)))
111	110	exbii 1881	. . . . . . . . . . . 12 ⊢ (∃𝑦(𝑣 ∈ 𝑦 ∧ ∀𝑧 ¬ (𝑧 ∈ 𝑦 ∧ (𝑧 ∩ 𝑦) = ∅)) ↔ ∃𝑦(𝑣 ∈ 𝑦 ∧ ∀𝑧(¬ 𝑧 ∈ 𝑦 ∨ ¬ (𝑧 ∩ 𝑦) = ∅)))
112	106, 108, 111	3bitr2i 302	. . . . . . . . . . 11 ⊢ (¬ ∀𝑦(𝑣 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅) ↔ ∃𝑦(𝑣 ∈ 𝑦 ∧ ∀𝑧(¬ 𝑧 ∈ 𝑦 ∨ ¬ (𝑧 ∩ 𝑦) = ∅)))
113	51	albii 1852	. . . . . . . . . . . . 13 ⊢ (∀𝑧(𝑧 ∈ 𝑦 → ¬ (𝑧 ∩ 𝑦) = ∅) ↔ ∀𝑧(¬ 𝑧 ∈ 𝑦 ∨ ¬ (𝑧 ∩ 𝑦) = ∅))
114	113	anbi2i 635	. . . . . . . . . . . 12 ⊢ ((𝑣 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ (𝑧 ∩ 𝑦) = ∅)) ↔ (𝑣 ∈ 𝑦 ∧ ∀𝑧(¬ 𝑧 ∈ 𝑦 ∨ ¬ (𝑧 ∩ 𝑦) = ∅)))
115	114	exbii 1881	. . . . . . . . . . 11 ⊢ (∃𝑦(𝑣 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ (𝑧 ∩ 𝑦) = ∅)) ↔ ∃𝑦(𝑣 ∈ 𝑦 ∧ ∀𝑧(¬ 𝑧 ∈ 𝑦 ∨ ¬ (𝑧 ∩ 𝑦) = ∅)))
116	112, 115	bitr4i 281	. . . . . . . . . 10 ⊢ (¬ ∀𝑦(𝑣 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅) ↔ ∃𝑦(𝑣 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ (𝑧 ∩ 𝑦) = ∅)))
117	55	anbi2i 635	. . . . . . . . . . 11 ⊢ ((𝑣 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ¬ (𝑧 ∩ 𝑦) = ∅) ↔ (𝑣 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ (𝑧 ∩ 𝑦) = ∅)))
118	117	exbii 1881	. . . . . . . . . 10 ⊢ (∃𝑦(𝑣 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ¬ (𝑧 ∩ 𝑦) = ∅) ↔ ∃𝑦(𝑣 ∈ 𝑦 ∧ ∀𝑧(𝑧 ∈ 𝑦 → ¬ (𝑧 ∩ 𝑦) = ∅)))
119	66	anbi2i 635	. . . . . . . . . . 11 ⊢ ((𝑣 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ¬ (𝑧 ∩ 𝑦) = ∅) ↔ (𝑣 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧))
120	119	exbii 1881	. . . . . . . . . 10 ⊢ (∃𝑦(𝑣 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ¬ (𝑧 ∩ 𝑦) = ∅) ↔ ∃𝑦(𝑣 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧))
121	116, 118, 120	3bitr2i 302	. . . . . . . . 9 ⊢ (¬ ∀𝑦(𝑣 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅) ↔ ∃𝑦(𝑣 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧))
122		olc 882	. . . . . . . . . 10 ⊢ (¬ ∀𝑦(𝑣 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅) → (¬ 𝑣 ∈ 𝑉 ∨ ¬ ∀𝑦(𝑣 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅)))
123		ianor 997	. . . . . . . . . . 11 ⊢ (¬ (𝑣 ∈ 𝑉 ∧ ∀𝑦(𝑣 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅)) ↔ (¬ 𝑣 ∈ 𝑉 ∨ ¬ ∀𝑦(𝑣 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅)))
124		elequ1 2154	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑣 → (𝑥 ∈ 𝑦 ↔ 𝑣 ∈ 𝑦))
125	124	imbi1d 344	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑣 → ((𝑥 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅) ↔ (𝑣 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅)))
126	125	albidv 1955	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑣 → (∀𝑦(𝑥 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅) ↔ ∀𝑦(𝑣 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅)))
127	126, 12	elrab2 3652	. . . . . . . . . . 11 ⊢ (𝑣 ∈ 𝑀 ↔ (𝑣 ∈ 𝑉 ∧ ∀𝑦(𝑣 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅)))
128	123, 127	xchnxbir 336	. . . . . . . . . 10 ⊢ (¬ 𝑣 ∈ 𝑀 ↔ (¬ 𝑣 ∈ 𝑉 ∨ ¬ ∀𝑦(𝑣 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅)))
129	122, 128	sylibr 237	. . . . . . . . 9 ⊢ (¬ ∀𝑦(𝑣 ∈ 𝑦 → ∃𝑧 ∈ 𝑦 (𝑧 ∩ 𝑦) = ∅) → ¬ 𝑣 ∈ 𝑀)
130	121, 129	sylbir 238	. . . . . . . 8 ⊢ (∃𝑦(𝑣 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧) → ¬ 𝑣 ∈ 𝑀)
131	130	anim1i 627	. . . . . . 7 ⊢ ((∃𝑦(𝑣 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧) ∧ 𝑣 ∈ 𝑀) → (¬ 𝑣 ∈ 𝑀 ∧ 𝑣 ∈ 𝑀))
132	100, 131	sylbi 220	. . . . . 6 ⊢ (∃𝑦((𝑣 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧) ∧ 𝑣 ∈ 𝑀) → (¬ 𝑣 ∈ 𝑀 ∧ 𝑣 ∈ 𝑀))
133	99, 132	sylbi 220	. . . . 5 ⊢ (∃𝑦(𝑣 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧 ∧ 𝑣 ∈ 𝑀) → (¬ 𝑣 ∈ 𝑀 ∧ 𝑣 ∈ 𝑀))
134	133	eximi 1868	. . . 4 ⊢ (∃𝑣∃𝑦(𝑣 ∈ 𝑦 ∧ ∀𝑧 ∈ 𝑦 ∃𝑤 ∈ 𝑦 𝑤 ∈ 𝑧 ∧ 𝑣 ∈ 𝑀) → ∃𝑣(¬ 𝑣 ∈ 𝑀 ∧ 𝑣 ∈ 𝑀))
135	97, 134	syl 18	. . 3 ⊢ (𝑀 ∈ 𝑉 → ∃𝑣(¬ 𝑣 ∈ 𝑀 ∧ 𝑣 ∈ 𝑀))
136	4, 135	mto 200	. 2 ⊢ ¬ 𝑀 ∈ 𝑉
137	136	nelir 3068	1 ⊢ 𝑀 ∉ 𝑉

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   ∧ w3a 1103  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2147   ∉ wnel 3065  ∀wral 3080  ∃wrex 3090  {crab 3416  Vcvv 3454   ∩ cin 4092  ∅c0 4281  {csn 4588

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-nel 3066  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-sn 4589  df-pr 4591

This theorem is used by:  mirimanofff  36629