Theorem elpssmo 36591

Description: Uniqueness of elements is equivalent to uniqueness of proper subsets. (Contributed by Adrian Ducourtial, 26-Oct-2026.)

Assertion

Ref	Expression
elpssmo	⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ ∃*𝑦 𝑦 ⊊ 𝐴)

Distinct variable group:   𝑦,𝐴,𝑥

Proof of Theorem elpssmo

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

Step	Hyp	Ref	Expression
1		0ex 5264	. . . . 5 ⊢ ∅ ∈ V
2	1	a1i 11	. . . 4 ⊢ (∃*𝑥 𝑥 ∈ 𝐴 → ∅ ∈ V)
3		pssss 4028	. . . . . . . . . . 11 ⊢ (𝑦 ⊊ 𝐴 → 𝑦 ⊆ 𝐴)
4	3	sseld 3912	. . . . . . . . . 10 ⊢ (𝑦 ⊊ 𝐴 → (𝑣 ∈ 𝑦 → 𝑣 ∈ 𝐴))
5	4	alrimiv 1961	. . . . . . . . 9 ⊢ (𝑦 ⊊ 𝐴 → ∀𝑣(𝑣 ∈ 𝑦 → 𝑣 ∈ 𝐴))
6		eleq1w 2847	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑣 → (𝑥 ∈ 𝐴 ↔ 𝑣 ∈ 𝐴))
7	6	cbvmovw 2630	. . . . . . . . . . . . . 14 ⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ ∃*𝑣 𝑣 ∈ 𝐴)
8		dfmo 2568	. . . . . . . . . . . . . . 15 ⊢ (∃*𝑣 𝑣 ∈ 𝐴 ↔ ∃𝑧∀𝑣(𝑣 ∈ 𝐴 → 𝑣 = 𝑧))
9		eleq1w 2847	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 = 𝑤 → (𝑣 ∈ 𝐴 ↔ 𝑤 ∈ 𝐴))
10		equequ1 2059	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑣 = 𝑤 → (𝑣 = 𝑧 ↔ 𝑤 = 𝑧))
11	9, 10	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑣 = 𝑤 → ((𝑣 ∈ 𝐴 → 𝑣 = 𝑧) ↔ (𝑤 ∈ 𝐴 → 𝑤 = 𝑧)))
12	11	spvv 2022	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (∀𝑣(𝑣 ∈ 𝐴 → 𝑣 = 𝑧) → (𝑤 ∈ 𝐴 → 𝑤 = 𝑧))
13	12	com12 33	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 ∈ 𝐴 → (∀𝑣(𝑣 ∈ 𝐴 → 𝑣 = 𝑧) → 𝑤 = 𝑧))
14		equcomiv 2048	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑤 = 𝑧 → 𝑧 = 𝑤)
15	13, 14	syl6 36	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 ∈ 𝐴 → (∀𝑣(𝑣 ∈ 𝐴 → 𝑣 = 𝑧) → 𝑧 = 𝑤))
16		equequ2 2060	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑧 = 𝑤 → (𝑣 = 𝑧 ↔ 𝑣 = 𝑤))
17	16	imbi2d 343	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑧 = 𝑤 → ((𝑣 ∈ 𝐴 → 𝑣 = 𝑧) ↔ (𝑣 ∈ 𝐴 → 𝑣 = 𝑤)))
18	17	albidv 1954	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑧 = 𝑤 → (∀𝑣(𝑣 ∈ 𝐴 → 𝑣 = 𝑧) ↔ ∀𝑣(𝑣 ∈ 𝐴 → 𝑣 = 𝑤)))
19	15, 18	syl6 36	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ 𝐴 → (∀𝑣(𝑣 ∈ 𝐴 → 𝑣 = 𝑧) → (∀𝑣(𝑣 ∈ 𝐴 → 𝑣 = 𝑧) ↔ ∀𝑣(𝑣 ∈ 𝐴 → 𝑣 = 𝑤))))
20	19	ibd 272	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 ∈ 𝐴 → (∀𝑣(𝑣 ∈ 𝐴 → 𝑣 = 𝑧) → ∀𝑣(𝑣 ∈ 𝐴 → 𝑣 = 𝑤)))
21	20	com12 33	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑣(𝑣 ∈ 𝐴 → 𝑣 = 𝑧) → (𝑤 ∈ 𝐴 → ∀𝑣(𝑣 ∈ 𝐴 → 𝑣 = 𝑤)))
22	21	exlimiv 1964	. . . . . . . . . . . . . . 15 ⊢ (∃𝑧∀𝑣(𝑣 ∈ 𝐴 → 𝑣 = 𝑧) → (𝑤 ∈ 𝐴 → ∀𝑣(𝑣 ∈ 𝐴 → 𝑣 = 𝑤)))
23	8, 22	sylbi 220	. . . . . . . . . . . . . 14 ⊢ (∃*𝑣 𝑣 ∈ 𝐴 → (𝑤 ∈ 𝐴 → ∀𝑣(𝑣 ∈ 𝐴 → 𝑣 = 𝑤)))
24	7, 23	sylbi 220	. . . . . . . . . . . . 13 ⊢ (∃*𝑥 𝑥 ∈ 𝐴 → (𝑤 ∈ 𝐴 → ∀𝑣(𝑣 ∈ 𝐴 → 𝑣 = 𝑤)))
25		elequ1 2153	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 = 𝑤 → (𝑣 ∈ 𝑦 ↔ 𝑤 ∈ 𝑦))
26	25	notbid 321	. . . . . . . . . . . . . . . 16 ⊢ (𝑣 = 𝑤 → (¬ 𝑣 ∈ 𝑦 ↔ ¬ 𝑤 ∈ 𝑦))
27	26	biimprcd 253	. . . . . . . . . . . . . . 15 ⊢ (¬ 𝑤 ∈ 𝑦 → (𝑣 = 𝑤 → ¬ 𝑣 ∈ 𝑦))
28	27	imim2d 58	. . . . . . . . . . . . . 14 ⊢ (¬ 𝑤 ∈ 𝑦 → ((𝑣 ∈ 𝐴 → 𝑣 = 𝑤) → (𝑣 ∈ 𝐴 → ¬ 𝑣 ∈ 𝑦)))
29	28	alimdv 1950	. . . . . . . . . . . . 13 ⊢ (¬ 𝑤 ∈ 𝑦 → (∀𝑣(𝑣 ∈ 𝐴 → 𝑣 = 𝑤) → ∀𝑣(𝑣 ∈ 𝐴 → ¬ 𝑣 ∈ 𝑦)))
30	24, 29	syl9 78	. . . . . . . . . . . 12 ⊢ (∃*𝑥 𝑥 ∈ 𝐴 → (¬ 𝑤 ∈ 𝑦 → (𝑤 ∈ 𝐴 → ∀𝑣(𝑣 ∈ 𝐴 → ¬ 𝑣 ∈ 𝑦))))
31	30	impcomd 417	. . . . . . . . . . 11 ⊢ (∃*𝑥 𝑥 ∈ 𝐴 → ((𝑤 ∈ 𝐴 ∧ ¬ 𝑤 ∈ 𝑦) → ∀𝑣(𝑣 ∈ 𝐴 → ¬ 𝑣 ∈ 𝑦)))
32	31	exlimdv 1967	. . . . . . . . . 10 ⊢ (∃*𝑥 𝑥 ∈ 𝐴 → (∃𝑤(𝑤 ∈ 𝐴 ∧ ¬ 𝑤 ∈ 𝑦) → ∀𝑣(𝑣 ∈ 𝐴 → ¬ 𝑣 ∈ 𝑦)))
33		pssnel 4427	. . . . . . . . . 10 ⊢ (𝑦 ⊊ 𝐴 → ∃𝑤(𝑤 ∈ 𝐴 ∧ ¬ 𝑤 ∈ 𝑦))
34	32, 33	impel 515	. . . . . . . . 9 ⊢ ((∃*𝑥 𝑥 ∈ 𝐴 ∧ 𝑦 ⊊ 𝐴) → ∀𝑣(𝑣 ∈ 𝐴 → ¬ 𝑣 ∈ 𝑦))
35		alsyl 1927	. . . . . . . . 9 ⊢ ((∀𝑣(𝑣 ∈ 𝑦 → 𝑣 ∈ 𝐴) ∧ ∀𝑣(𝑣 ∈ 𝐴 → ¬ 𝑣 ∈ 𝑦)) → ∀𝑣(𝑣 ∈ 𝑦 → ¬ 𝑣 ∈ 𝑦))
36	5, 34, 35	syl2an2 699	. . . . . . . 8 ⊢ ((∃*𝑥 𝑥 ∈ 𝐴 ∧ 𝑦 ⊊ 𝐴) → ∀𝑣(𝑣 ∈ 𝑦 → ¬ 𝑣 ∈ 𝑦))
37		pm2.01 190	. . . . . . . 8 ⊢ ((𝑣 ∈ 𝑦 → ¬ 𝑣 ∈ 𝑦) → ¬ 𝑣 ∈ 𝑦)
38	36, 37	sylg 1855	. . . . . . 7 ⊢ ((∃*𝑥 𝑥 ∈ 𝐴 ∧ 𝑦 ⊊ 𝐴) → ∀𝑣 ¬ 𝑣 ∈ 𝑦)
39		eq0 4300	. . . . . . 7 ⊢ (𝑦 = ∅ ↔ ∀𝑣 ¬ 𝑣 ∈ 𝑦)
40	38, 39	sylibr 237	. . . . . 6 ⊢ ((∃*𝑥 𝑥 ∈ 𝐴 ∧ 𝑦 ⊊ 𝐴) → 𝑦 = ∅)
41	40	ex 418	. . . . 5 ⊢ (∃*𝑥 𝑥 ∈ 𝐴 → (𝑦 ⊊ 𝐴 → 𝑦 = ∅))
42	41	alrimiv 1961	. . . 4 ⊢ (∃*𝑥 𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ⊊ 𝐴 → 𝑦 = ∅))
43		eqeq2 2775	. . . . . 6 ⊢ (𝑢 = ∅ → (𝑦 = 𝑢 ↔ 𝑦 = ∅))
44	43	imbi2d 343	. . . . 5 ⊢ (𝑢 = ∅ → ((𝑦 ⊊ 𝐴 → 𝑦 = 𝑢) ↔ (𝑦 ⊊ 𝐴 → 𝑦 = ∅)))
45	44	albidv 1954	. . . 4 ⊢ (𝑢 = ∅ → (∀𝑦(𝑦 ⊊ 𝐴 → 𝑦 = 𝑢) ↔ ∀𝑦(𝑦 ⊊ 𝐴 → 𝑦 = ∅)))
46	2, 42, 45	spcedv 3556	. . 3 ⊢ (∃*𝑥 𝑥 ∈ 𝐴 → ∃𝑢∀𝑦(𝑦 ⊊ 𝐴 → 𝑦 = 𝑢))
47		dfmo 2568	. . 3 ⊢ (∃*𝑦 𝑦 ⊊ 𝐴 ↔ ∃𝑢∀𝑦(𝑦 ⊊ 𝐴 → 𝑦 = 𝑢))
48	46, 47	sylibr 237	. 2 ⊢ (∃*𝑥 𝑥 ∈ 𝐴 → ∃*𝑦 𝑦 ⊊ 𝐴)
49		vsnid 4624	. . . . . . . . 9 ⊢ 𝑥 ∈ {𝑥}
50	49	n0ii 4292	. . . . . . . 8 ⊢ ¬ {𝑥} = ∅
51		simp1 1154	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ ¬ 𝑣 = 𝑥) → 𝑥 ∈ 𝐴)
52		velsn 4600	. . . . . . . . . . . . . . . . 17 ⊢ (𝑣 ∈ {𝑥} ↔ 𝑣 = 𝑥)
53	52	notbii 323	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑣 ∈ {𝑥} ↔ ¬ 𝑣 = 𝑥)
54		ssnelpss 4045	. . . . . . . . . . . . . . . . 17 ⊢ ({𝑥} ⊆ 𝐴 → ((𝑣 ∈ 𝐴 ∧ ¬ 𝑣 ∈ {𝑥}) → {𝑥} ⊊ 𝐴))
55		snssi 4746	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ 𝐴 → {𝑥} ⊆ 𝐴)
56	54, 55	syl11 34	. . . . . . . . . . . . . . . 16 ⊢ ((𝑣 ∈ 𝐴 ∧ ¬ 𝑣 ∈ {𝑥}) → (𝑥 ∈ 𝐴 → {𝑥} ⊊ 𝐴))
57	53, 56	sylan2br 607	. . . . . . . . . . . . . . 15 ⊢ ((𝑣 ∈ 𝐴 ∧ ¬ 𝑣 = 𝑥) → (𝑥 ∈ 𝐴 → {𝑥} ⊊ 𝐴))
58	57	ex 418	. . . . . . . . . . . . . 14 ⊢ (𝑣 ∈ 𝐴 → (¬ 𝑣 = 𝑥 → (𝑥 ∈ 𝐴 → {𝑥} ⊊ 𝐴)))
59	58	com23 87	. . . . . . . . . . . . 13 ⊢ (𝑣 ∈ 𝐴 → (𝑥 ∈ 𝐴 → (¬ 𝑣 = 𝑥 → {𝑥} ⊊ 𝐴)))
60	59	3imp21 1131	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ ¬ 𝑣 = 𝑥) → {𝑥} ⊊ 𝐴)
61		noel 4286	. . . . . . . . . . . . . 14 ⊢ ¬ 𝑥 ∈ ∅
62		0ss 4353	. . . . . . . . . . . . . . 15 ⊢ ∅ ⊆ 𝐴
63		ssnelpss 4045	. . . . . . . . . . . . . . 15 ⊢ (∅ ⊆ 𝐴 → ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ∅) → ∅ ⊊ 𝐴))
64	62, 63	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ ∅) → ∅ ⊊ 𝐴)
65	61, 64	mpan2 704	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ 𝐴 → ∅ ⊊ 𝐴)
66		psseq1 4020	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = 𝑤 → (𝑦 ⊊ 𝐴 ↔ 𝑤 ⊊ 𝐴))
67	66	mo4 2594	. . . . . . . . . . . . . . . . 17 ⊢ (∃*𝑦 𝑦 ⊊ 𝐴 ↔ ∀𝑦∀𝑤((𝑦 ⊊ 𝐴 ∧ 𝑤 ⊊ 𝐴) → 𝑦 = 𝑤))
68		vsnex 5397	. . . . . . . . . . . . . . . . . 18 ⊢ {𝑥} ∈ V
69		psseq1 4020	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑦 = {𝑥} → (𝑦 ⊊ 𝐴 ↔ {𝑥} ⊊ 𝐴))
70	69	anbi1d 643	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = {𝑥} → ((𝑦 ⊊ 𝐴 ∧ 𝑤 ⊊ 𝐴) ↔ ({𝑥} ⊊ 𝐴 ∧ 𝑤 ⊊ 𝐴)))
71		eqeq1 2767	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 = {𝑥} → (𝑦 = 𝑤 ↔ {𝑥} = 𝑤))
72	70, 71	imbi12d 347	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = {𝑥} → (((𝑦 ⊊ 𝐴 ∧ 𝑤 ⊊ 𝐴) → 𝑦 = 𝑤) ↔ (({𝑥} ⊊ 𝐴 ∧ 𝑤 ⊊ 𝐴) → {𝑥} = 𝑤)))
73	72	albidv 1954	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 = {𝑥} → (∀𝑤((𝑦 ⊊ 𝐴 ∧ 𝑤 ⊊ 𝐴) → 𝑦 = 𝑤) ↔ ∀𝑤(({𝑥} ⊊ 𝐴 ∧ 𝑤 ⊊ 𝐴) → {𝑥} = 𝑤)))
74	68, 73	spcv 3563	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑦∀𝑤((𝑦 ⊊ 𝐴 ∧ 𝑤 ⊊ 𝐴) → 𝑦 = 𝑤) → ∀𝑤(({𝑥} ⊊ 𝐴 ∧ 𝑤 ⊊ 𝐴) → {𝑥} = 𝑤))
75	67, 74	sylbi 220	. . . . . . . . . . . . . . . 16 ⊢ (∃*𝑦 𝑦 ⊊ 𝐴 → ∀𝑤(({𝑥} ⊊ 𝐴 ∧ 𝑤 ⊊ 𝐴) → {𝑥} = 𝑤))
76		psseq1 4020	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑤 = ∅ → (𝑤 ⊊ 𝐴 ↔ ∅ ⊊ 𝐴))
77	76	anbi2d 642	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = ∅ → (({𝑥} ⊊ 𝐴 ∧ 𝑤 ⊊ 𝐴) ↔ ({𝑥} ⊊ 𝐴 ∧ ∅ ⊊ 𝐴)))
78		eqeq2 2775	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 = ∅ → ({𝑥} = 𝑤 ↔ {𝑥} = ∅))
79	77, 78	imbi12d 347	. . . . . . . . . . . . . . . . 17 ⊢ (𝑤 = ∅ → ((({𝑥} ⊊ 𝐴 ∧ 𝑤 ⊊ 𝐴) → {𝑥} = 𝑤) ↔ (({𝑥} ⊊ 𝐴 ∧ ∅ ⊊ 𝐴) → {𝑥} = ∅)))
80	1, 79	spcv 3563	. . . . . . . . . . . . . . . 16 ⊢ (∀𝑤(({𝑥} ⊊ 𝐴 ∧ 𝑤 ⊊ 𝐴) → {𝑥} = 𝑤) → (({𝑥} ⊊ 𝐴 ∧ ∅ ⊊ 𝐴) → {𝑥} = ∅))
81	75, 80	syl 18	. . . . . . . . . . . . . . 15 ⊢ (∃*𝑦 𝑦 ⊊ 𝐴 → (({𝑥} ⊊ 𝐴 ∧ ∅ ⊊ 𝐴) → {𝑥} = ∅))
82	81	ancomsd 471	. . . . . . . . . . . . . 14 ⊢ (∃*𝑦 𝑦 ⊊ 𝐴 → ((∅ ⊊ 𝐴 ∧ {𝑥} ⊊ 𝐴) → {𝑥} = ∅))
83	82	com12 33	. . . . . . . . . . . . 13 ⊢ ((∅ ⊊ 𝐴 ∧ {𝑥} ⊊ 𝐴) → (∃*𝑦 𝑦 ⊊ 𝐴 → {𝑥} = ∅))
84	65, 83	sylan 592	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ 𝐴 ∧ {𝑥} ⊊ 𝐴) → (∃*𝑦 𝑦 ⊊ 𝐴 → {𝑥} = ∅))
85	51, 60, 84	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ ¬ 𝑣 = 𝑥) → (∃*𝑦 𝑦 ⊊ 𝐴 → {𝑥} = ∅))
86	85	3expia 1139	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → (¬ 𝑣 = 𝑥 → (∃*𝑦 𝑦 ⊊ 𝐴 → {𝑥} = ∅)))
87	86	com23 87	. . . . . . . . 9 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → (∃*𝑦 𝑦 ⊊ 𝐴 → (¬ 𝑣 = 𝑥 → {𝑥} = ∅)))
88	87	3impia 1135	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ ∃*𝑦 𝑦 ⊊ 𝐴) → (¬ 𝑣 = 𝑥 → {𝑥} = ∅))
89	50, 88	mt3i 150	. . . . . . 7 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ ∃*𝑦 𝑦 ⊊ 𝐴) → 𝑣 = 𝑥)
90	89	3comr 1143	. . . . . 6 ⊢ ((∃*𝑦 𝑦 ⊊ 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → 𝑣 = 𝑥)
91	90	equcomd 2053	. . . . 5 ⊢ ((∃*𝑦 𝑦 ⊊ 𝐴 ∧ 𝑥 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → 𝑥 = 𝑣)
92	91	3expib 1140	. . . 4 ⊢ (∃*𝑦 𝑦 ⊊ 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → 𝑥 = 𝑣))
93	92	alrimivv 1962	. . 3 ⊢ (∃*𝑦 𝑦 ⊊ 𝐴 → ∀𝑥∀𝑣((𝑥 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → 𝑥 = 𝑣))
94	6	mo4 2594	. . 3 ⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ ∀𝑥∀𝑣((𝑥 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴) → 𝑥 = 𝑣))
95	93, 94	sylibr 237	. 2 ⊢ (∃*𝑦 𝑦 ⊊ 𝐴 → ∃*𝑥 𝑥 ∈ 𝐴)
96	48, 95	impbii 212	1 ⊢ (∃*𝑥 𝑥 ∈ 𝐴 ↔ ∃*𝑦 𝑦 ⊊ 𝐴)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103  ∀wal 1567   = wceq 1569  ∃wex 1811   ∈ wcel 2146  ∃*wmo 2565  Vcvv 3454   ⊆ wss 3900   ⊊ wpss 4016  ∅c0 4281  {csn 4588

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 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-mo 2567  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-v 3456  df-ss 3901  df-pss 4017  df-dif 4050  df-un 4154  df-nul 4282  df-sn 4589  df-pr 4591

This theorem is used by:  elpsseu  36592