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	⊢ ( ∃ 𝑥 𝑥 ∈ 𝐴 ↔ ∃ 𝑦 𝑦 ⊊ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		0ss	⊢ ∅ ⊆ 𝐴
2	1	a1i	⊢ ( 𝑥 ∈ 𝐴 → ∅ ⊆ 𝐴 )
3		ne0i	⊢ ( 𝑥 ∈ 𝐴 → 𝐴 ≠ ∅ )
4	3	necomd	⊢ ( 𝑥 ∈ 𝐴 → ∅ ≠ 𝐴 )
5		df-pss	⊢ ( ∅ ⊊ 𝐴 ↔ ( ∅ ⊆ 𝐴 ∧ ∅ ≠ 𝐴 ) )
6	2 4 5	sylanbrc	⊢ ( 𝑥 ∈ 𝐴 → ∅ ⊊ 𝐴 )
7		0ex	⊢ ∅ ∈ V
8		psseq1	⊢ ( 𝑦 = ∅ → ( 𝑦 ⊊ 𝐴 ↔ ∅ ⊊ 𝐴 ) )
9	7 8	spcev	⊢ ( ∅ ⊊ 𝐴 → ∃ 𝑦 𝑦 ⊊ 𝐴 )
10	6 9	syl	⊢ ( 𝑥 ∈ 𝐴 → ∃ 𝑦 𝑦 ⊊ 𝐴 )
11	10	exlimiv	⊢ ( ∃ 𝑥 𝑥 ∈ 𝐴 → ∃ 𝑦 𝑦 ⊊ 𝐴 )
12		pssnel	⊢ ( 𝑦 ⊊ 𝐴 → ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝑦 ) )
13		exsimpl	⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ¬ 𝑥 ∈ 𝑦 ) → ∃ 𝑥 𝑥 ∈ 𝐴 )
14	12 13	syl	⊢ ( 𝑦 ⊊ 𝐴 → ∃ 𝑥 𝑥 ∈ 𝐴 )
15	14	exlimiv	⊢ ( ∃ 𝑦 𝑦 ⊊ 𝐴 → ∃ 𝑥 𝑥 ∈ 𝐴 )
16	11 15	impbii	⊢ ( ∃ 𝑥 𝑥 ∈ 𝐴 ↔ ∃ 𝑦 𝑦 ⊊ 𝐴 )