Theorem elpsseu

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

	Ref	Expression
Assertion	elpsseu	|- ( E! x x e. A <-> E! y y C. A )

Proof

Step	Hyp	Ref	Expression
1		elpssex	|- ( E. x x e. A <-> E. y y C. A )
2		elpssmo	|- ( E* x x e. A <-> E* y y C. A )
3	1 2	anbi12i	|- ( ( E. x x e. A /\ E* x x e. A ) <-> ( E. y y C. A /\ E* y y C. A ) )
4		df-eu	|- ( E! x x e. A <-> ( E. x x e. A /\ E* x x e. A ) )
5		df-eu	|- ( E! y y C. A <-> ( E. y y C. A /\ E* y y C. A ) )
6	3 4 5	3bitr4i	|- ( E! x x e. A <-> E! y y C. A )