Theorem sels

Description: If a class is a set, then it is a member of a set. (Contributed by BJ, 3-Apr-2019)

	Ref	Expression
Assertion	sels	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 𝐴 ∈ 𝑥 )

Proof

Step	Hyp	Ref	Expression
1		snidg	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 } )
2		snex	⊢ { 𝐴 } ∈ V
3		eleq2	⊢ ( 𝑥 = { 𝐴 } → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ { 𝐴 } ) )
4	2 3	spcev	⊢ ( 𝐴 ∈ { 𝐴 } → ∃ 𝑥 𝐴 ∈ 𝑥 )
5	1 4	syl	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 𝐴 ∈ 𝑥 )