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	|- ( E. x x e. A <-> E. y y C. A )

Proof

Step	Hyp	Ref	Expression
1		0ss	|- (/) C_ A
2	1	a1i	|- ( x e. A -> (/) C_ A )
3		ne0i	|- ( x e. A -> A =/= (/) )
4	3	necomd	|- ( x e. A -> (/) =/= A )
5		df-pss	|- ( (/) C. A <-> ( (/) C_ A /\ (/) =/= A ) )
6	2 4 5	sylanbrc	|- ( x e. A -> (/) C. A )
7		0ex	|- (/) e. _V
8		psseq1	|- ( y = (/) -> ( y C. A <-> (/) C. A ) )
9	7 8	spcev	|- ( (/) C. A -> E. y y C. A )
10	6 9	syl	|- ( x e. A -> E. y y C. A )
11	10	exlimiv	|- ( E. x x e. A -> E. y y C. A )
12		pssnel	|- ( y C. A -> E. x ( x e. A /\ -. x e. y ) )
13		exsimpl	|- ( E. x ( x e. A /\ -. x e. y ) -> E. x x e. A )
14	12 13	syl	|- ( y C. A -> E. x x e. A )
15	14	exlimiv	|- ( E. y y C. A -> E. x x e. A )
16	11 15	impbii	|- ( E. x x e. A <-> E. y y C. A )