Theorem elpssex

Description: A class has an element just in case it has a proper subset. (Contributed by Adrian Ducourtial, 26-Oct-2026)

	Ref	Expression
Assertion	elpssex	$$⊢\exists xx\in A\leftrightarrow \exists yy\subset A$$

Proof

Step	Hyp	Ref	Expression
1		0ss	$$⊢\varnothing \subseteq A$$
2	1	a1i	$$⊢x\in A\to \varnothing \subseteq A$$
3		ne0i	$$⊢x\in A\to A\ne \varnothing$$
4	3	necomd	$$⊢x\in A\to \varnothing \ne A$$
5		df-pss	$$⊢\varnothing \subset A\leftrightarrow \left(\varnothing \subseteq A\wedge \varnothing \ne A\right)$$
6	2 4 5	sylanbrc	$$⊢x\in A\to \varnothing \subset A$$
7		0ex	$$⊢\varnothing \in \mathrm{V}$$
8		psseq1	$$⊢y=\varnothing \to \left(y\subset A\leftrightarrow \varnothing \subset A\right)$$
9	7 8	spcev	$$⊢\varnothing \subset A\to \exists yy\subset A$$
10	6 9	syl	$$⊢x\in A\to \exists yy\subset A$$
11	10	exlimiv	$$⊢\exists xx\in A\to \exists yy\subset A$$
12		pssnel	$$⊢y\subset A\to \exists x\left(x\in A\wedge \neg x\in y\right)$$
13		exsimpl	$$⊢\exists x\left(x\in A\wedge \neg x\in y\right)\to \exists xx\in A$$
14	12 13	syl	$$⊢y\subset A\to \exists xx\in A$$
15	14	exlimiv	$$⊢\exists yy\subset A\to \exists xx\in A$$
16	11 15	impbii	$$⊢\exists xx\in A\leftrightarrow \exists yy\subset A$$