Theorem elpssmo

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

	Ref	Expression
Assertion	elpssmo	$$⊢{\exists }^{*}xx\in A\leftrightarrow {\exists }^{*}yy\subset A$$

Proof

Step	Hyp	Ref	Expression
1		0ex	$$⊢\varnothing \in \mathrm{V}$$
2	1	a1i	$$⊢{\exists }^{*}xx\in A\to \varnothing \in \mathrm{V}$$
3		pssss	$$⊢y\subset A\to y\subseteq A$$
4	3	sseld	$$⊢y\subset A\to \left(v\in y\to v\in A\right)$$
5	4	alrimiv	$$⊢y\subset A\to \forall v\left(v\in y\to v\in A\right)$$
6		eleq1w	$$⊢x=v\to \left(x\in A\leftrightarrow v\in A\right)$$
7	6	cbvmovw	$$⊢{\exists }^{*}xx\in A\leftrightarrow {\exists }^{*}vv\in A$$
8		dfmo	$$⊢{\exists }^{*}vv\in A\leftrightarrow \exists z\forall v\left(v\in A\to v=z\right)$$
9		eleq1w	$$⊢v=w\to \left(v\in A\leftrightarrow w\in A\right)$$
10		equequ1	$$⊢v=w\to \left(v=z\leftrightarrow w=z\right)$$
11	9 10	imbi12d	$$⊢v=w\to \left(\left(v\in A\to v=z\right)\leftrightarrow \left(w\in A\to w=z\right)\right)$$
12	11	spvv	$$⊢\forall v\left(v\in A\to v=z\right)\to \left(w\in A\to w=z\right)$$
13	12	com12	$$⊢w\in A\to \left(\forall v\left(v\in A\to v=z\right)\to w=z\right)$$
14		equcomiv	$$⊢w=z\to z=w$$
15	13 14	syl6	$$⊢w\in A\to \left(\forall v\left(v\in A\to v=z\right)\to z=w\right)$$
16		equequ2	$$⊢z=w\to \left(v=z\leftrightarrow v=w\right)$$
17	16	imbi2d	$$⊢z=w\to \left(\left(v\in A\to v=z\right)\leftrightarrow \left(v\in A\to v=w\right)\right)$$
18	17	albidv	$$⊢z=w\to \left(\forall v\left(v\in A\to v=z\right)\leftrightarrow \forall v\left(v\in A\to v=w\right)\right)$$
19	15 18	syl6	$$⊢w\in A\to \left(\forall v\left(v\in A\to v=z\right)\to \left(\forall v\left(v\in A\to v=z\right)\leftrightarrow \forall v\left(v\in A\to v=w\right)\right)\right)$$
20	19	ibd	$$⊢w\in A\to \left(\forall v\left(v\in A\to v=z\right)\to \forall v\left(v\in A\to v=w\right)\right)$$
21	20	com12	$$⊢\forall v\left(v\in A\to v=z\right)\to \left(w\in A\to \forall v\left(v\in A\to v=w\right)\right)$$
22	21	exlimiv	$$⊢\exists z\forall v\left(v\in A\to v=z\right)\to \left(w\in A\to \forall v\left(v\in A\to v=w\right)\right)$$
23	8 22	sylbi	$$⊢{\exists }^{*}vv\in A\to \left(w\in A\to \forall v\left(v\in A\to v=w\right)\right)$$
24	7 23	sylbi	$$⊢{\exists }^{*}xx\in A\to \left(w\in A\to \forall v\left(v\in A\to v=w\right)\right)$$
25		elequ1	$$⊢v=w\to \left(v\in y\leftrightarrow w\in y\right)$$
26	25	notbid	$$⊢v=w\to \left(\neg v\in y\leftrightarrow \neg w\in y\right)$$
27	26	biimprcd	$$⊢\neg w\in y\to \left(v=w\to \neg v\in y\right)$$
28	27	imim2d	$$⊢\neg w\in y\to \left(\left(v\in A\to v=w\right)\to \left(v\in A\to \neg v\in y\right)\right)$$
29	28	alimdv	$$⊢\neg w\in y\to \left(\forall v\left(v\in A\to v=w\right)\to \forall v\left(v\in A\to \neg v\in y\right)\right)$$
30	24 29	syl9	$$⊢{\exists }^{*}xx\in A\to \left(\neg w\in y\to \left(w\in A\to \forall v\left(v\in A\to \neg v\in y\right)\right)\right)$$
31	30	impcomd	$$⊢{\exists }^{*}xx\in A\to \left(\left(w\in A\wedge \neg w\in y\right)\to \forall v\left(v\in A\to \neg v\in y\right)\right)$$
32	31	exlimdv	$$⊢{\exists }^{*}xx\in A\to \left(\exists w\left(w\in A\wedge \neg w\in y\right)\to \forall v\left(v\in A\to \neg v\in y\right)\right)$$
33		pssnel	$$⊢y\subset A\to \exists w\left(w\in A\wedge \neg w\in y\right)$$
34	32 33	impel	$$⊢\left({\exists }^{*}xx\in A\wedge y\subset A\right)\to \forall v\left(v\in A\to \neg v\in y\right)$$
35		alsyl	$$⊢\left(\forall v\left(v\in y\to v\in A\right)\wedge \forall v\left(v\in A\to \neg v\in y\right)\right)\to \forall v\left(v\in y\to \neg v\in y\right)$$
36	5 34 35	syl2an2	$$⊢\left({\exists }^{*}xx\in A\wedge y\subset A\right)\to \forall v\left(v\in y\to \neg v\in y\right)$$
37		pm2.01	$$⊢\left(v\in y\to \neg v\in y\right)\to \neg v\in y$$
38	36 37	sylg	$$⊢\left({\exists }^{*}xx\in A\wedge y\subset A\right)\to \forall v\neg v\in y$$
39		eq0	$$⊢y=\varnothing \leftrightarrow \forall v\neg v\in y$$
40	38 39	sylibr	$$⊢\left({\exists }^{*}xx\in A\wedge y\subset A\right)\to y=\varnothing$$
41	40	ex	$$⊢{\exists }^{*}xx\in A\to \left(y\subset A\to y=\varnothing \right)$$
42	41	alrimiv	$$⊢{\exists }^{*}xx\in A\to \forall y\left(y\subset A\to y=\varnothing \right)$$
43		eqeq2	$$⊢u=\varnothing \to \left(y=u\leftrightarrow y=\varnothing \right)$$
44	43	imbi2d	$$⊢u=\varnothing \to \left(\left(y\subset A\to y=u\right)\leftrightarrow \left(y\subset A\to y=\varnothing \right)\right)$$
45	44	albidv	$$⊢u=\varnothing \to \left(\forall y\left(y\subset A\to y=u\right)\leftrightarrow \forall y\left(y\subset A\to y=\varnothing \right)\right)$$
46	2 42 45	spcedv	$$⊢{\exists }^{*}xx\in A\to \exists u\forall y\left(y\subset A\to y=u\right)$$
47		dfmo	$$⊢{\exists }^{*}yy\subset A\leftrightarrow \exists u\forall y\left(y\subset A\to y=u\right)$$
48	46 47	sylibr	$$⊢{\exists }^{*}xx\in A\to {\exists }^{*}yy\subset A$$
49		vsnid	$$⊢x\in \left\{x\right\}$$
50	49	n0ii	$$⊢\neg \left\{x\right\}=\varnothing$$
51		simp1	$$⊢\left(x\in A\wedge v\in A\wedge \neg v=x\right)\to x\in A$$
52		velsn	$$⊢v\in \left\{x\right\}\leftrightarrow v=x$$
53	52	notbii	$$⊢\neg v\in \left\{x\right\}\leftrightarrow \neg v=x$$
54		ssnelpss	$$⊢\left\{x\right\}\subseteq A\to \left(\left(v\in A\wedge \neg v\in \left\{x\right\}\right)\to \left\{x\right\}\subset A\right)$$
55		snssi	$$⊢x\in A\to \left\{x\right\}\subseteq A$$
56	54 55	syl11	$$⊢\left(v\in A\wedge \neg v\in \left\{x\right\}\right)\to \left(x\in A\to \left\{x\right\}\subset A\right)$$
57	53 56	sylan2br	$$⊢\left(v\in A\wedge \neg v=x\right)\to \left(x\in A\to \left\{x\right\}\subset A\right)$$
58	57	ex	$$⊢v\in A\to \left(\neg v=x\to \left(x\in A\to \left\{x\right\}\subset A\right)\right)$$
59	58	com23	$$⊢v\in A\to \left(x\in A\to \left(\neg v=x\to \left\{x\right\}\subset A\right)\right)$$
60	59	3imp21	$$⊢\left(x\in A\wedge v\in A\wedge \neg v=x\right)\to \left\{x\right\}\subset A$$
61		noel	$$⊢\neg x\in \varnothing$$
62		0ss	$$⊢\varnothing \subseteq A$$
63		ssnelpss	$$⊢\varnothing \subseteq A\to \left(\left(x\in A\wedge \neg x\in \varnothing \right)\to \varnothing \subset A\right)$$
64	62 63	ax-mp	$$⊢\left(x\in A\wedge \neg x\in \varnothing \right)\to \varnothing \subset A$$
65	61 64	mpan2	$$⊢x\in A\to \varnothing \subset A$$
66		psseq1	$$⊢y=w\to \left(y\subset A\leftrightarrow w\subset A\right)$$
67	66	mo4	$$⊢{\exists }^{*}yy\subset A\leftrightarrow \forall y\forall w\left(\left(y\subset A\wedge w\subset A\right)\to y=w\right)$$
68		vsnex	$$⊢\left\{x\right\}\in \mathrm{V}$$
69		psseq1	$$⊢y=\left\{x\right\}\to \left(y\subset A\leftrightarrow \left\{x\right\}\subset A\right)$$
70	69	anbi1d	$$⊢y=\left\{x\right\}\to \left(\left(y\subset A\wedge w\subset A\right)\leftrightarrow \left(\left\{x\right\}\subset A\wedge w\subset A\right)\right)$$
71		eqeq1	$$⊢y=\left\{x\right\}\to \left(y=w\leftrightarrow \left\{x\right\}=w\right)$$
72	70 71	imbi12d	$$⊢y=\left\{x\right\}\to \left(\left(\left(y\subset A\wedge w\subset A\right)\to y=w\right)\leftrightarrow \left(\left(\left\{x\right\}\subset A\wedge w\subset A\right)\to \left\{x\right\}=w\right)\right)$$
73	72	albidv	$$⊢y=\left\{x\right\}\to \left(\forall w\left(\left(y\subset A\wedge w\subset A\right)\to y=w\right)\leftrightarrow \forall w\left(\left(\left\{x\right\}\subset A\wedge w\subset A\right)\to \left\{x\right\}=w\right)\right)$$
74	68 73	spcv	$$⊢\forall y\forall w\left(\left(y\subset A\wedge w\subset A\right)\to y=w\right)\to \forall w\left(\left(\left\{x\right\}\subset A\wedge w\subset A\right)\to \left\{x\right\}=w\right)$$
75	67 74	sylbi	$$⊢{\exists }^{*}yy\subset A\to \forall w\left(\left(\left\{x\right\}\subset A\wedge w\subset A\right)\to \left\{x\right\}=w\right)$$
76		psseq1	$$⊢w=\varnothing \to \left(w\subset A\leftrightarrow \varnothing \subset A\right)$$
77	76	anbi2d	$$⊢w=\varnothing \to \left(\left(\left\{x\right\}\subset A\wedge w\subset A\right)\leftrightarrow \left(\left\{x\right\}\subset A\wedge \varnothing \subset A\right)\right)$$
78		eqeq2	$$⊢w=\varnothing \to \left(\left\{x\right\}=w\leftrightarrow \left\{x\right\}=\varnothing \right)$$
79	77 78	imbi12d	$$⊢w=\varnothing \to \left(\left(\left(\left\{x\right\}\subset A\wedge w\subset A\right)\to \left\{x\right\}=w\right)\leftrightarrow \left(\left(\left\{x\right\}\subset A\wedge \varnothing \subset A\right)\to \left\{x\right\}=\varnothing \right)\right)$$
80	1 79	spcv	$$⊢\forall w\left(\left(\left\{x\right\}\subset A\wedge w\subset A\right)\to \left\{x\right\}=w\right)\to \left(\left(\left\{x\right\}\subset A\wedge \varnothing \subset A\right)\to \left\{x\right\}=\varnothing \right)$$
81	75 80	syl	$$⊢{\exists }^{*}yy\subset A\to \left(\left(\left\{x\right\}\subset A\wedge \varnothing \subset A\right)\to \left\{x\right\}=\varnothing \right)$$
82	81	ancomsd	$$⊢{\exists }^{*}yy\subset A\to \left(\left(\varnothing \subset A\wedge \left\{x\right\}\subset A\right)\to \left\{x\right\}=\varnothing \right)$$
83	82	com12	$$⊢\left(\varnothing \subset A\wedge \left\{x\right\}\subset A\right)\to \left({\exists }^{*}yy\subset A\to \left\{x\right\}=\varnothing \right)$$
84	65 83	sylan	$$⊢\left(x\in A\wedge \left\{x\right\}\subset A\right)\to \left({\exists }^{*}yy\subset A\to \left\{x\right\}=\varnothing \right)$$
85	51 60 84	syl2anc	$$⊢\left(x\in A\wedge v\in A\wedge \neg v=x\right)\to \left({\exists }^{*}yy\subset A\to \left\{x\right\}=\varnothing \right)$$
86	85	3expia	$$⊢\left(x\in A\wedge v\in A\right)\to \left(\neg v=x\to \left({\exists }^{*}yy\subset A\to \left\{x\right\}=\varnothing \right)\right)$$
87	86	com23	$$⊢\left(x\in A\wedge v\in A\right)\to \left({\exists }^{*}yy\subset A\to \left(\neg v=x\to \left\{x\right\}=\varnothing \right)\right)$$
88	87	3impia	$$⊢\left(x\in A\wedge v\in A\wedge {\exists }^{*}yy\subset A\right)\to \left(\neg v=x\to \left\{x\right\}=\varnothing \right)$$
89	50 88	mt3i	$$⊢\left(x\in A\wedge v\in A\wedge {\exists }^{*}yy\subset A\right)\to v=x$$
90	89	3comr	$$⊢\left({\exists }^{*}yy\subset A\wedge x\in A\wedge v\in A\right)\to v=x$$
91	90	equcomd	$$⊢\left({\exists }^{*}yy\subset A\wedge x\in A\wedge v\in A\right)\to x=v$$
92	91	3expib	$$⊢{\exists }^{*}yy\subset A\to \left(\left(x\in A\wedge v\in A\right)\to x=v\right)$$
93	92	alrimivv	$$⊢{\exists }^{*}yy\subset A\to \forall x\forall v\left(\left(x\in A\wedge v\in A\right)\to x=v\right)$$
94	6	mo4	$$⊢{\exists }^{*}xx\in A\leftrightarrow \forall x\forall v\left(\left(x\in A\wedge v\in A\right)\to x=v\right)$$
95	93 94	sylibr	$$⊢{\exists }^{*}yy\subset A\to {\exists }^{*}xx\in A$$
96	48 95	impbii	$$⊢{\exists }^{*}xx\in A\leftrightarrow {\exists }^{*}yy\subset A$$