Theorem velsn

Description: There is only one element in a singleton. Exercise 2 of TakeutiZaring p. 15. (Contributed by NM, 21-Jun-1993)

	Ref	Expression
Assertion	velsn	⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2	1	elsn	⊢ ( 𝑥 ∈ { 𝐴 } ↔ 𝑥 = 𝐴 )