Theorem snid

Description: A set is a member of its singleton. Part of Theorem 7.6 of Quine p. 49. (Contributed by NM, 31-Dec-1993)

	Ref	Expression
Hypothesis	snid.1	⊢ 𝐴 ∈ V
Assertion	snid	⊢ 𝐴 ∈ { 𝐴 }

Proof

Step	Hyp	Ref	Expression
1		snid.1	⊢ 𝐴 ∈ V
2		snidb	⊢ ( 𝐴 ∈ V ↔ 𝐴 ∈ { 𝐴 } )
3	1 2	mpbi	⊢ 𝐴 ∈ { 𝐴 }