Theorem elpssmo

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

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

Proof

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