Theorem bj-snex

Description: A singleton is a set. See also snex , snexALT . (Contributed by NM, 7-Aug-1994) Prove it from ax-bj-sn . (Revised by BJ, 12-Jan-2025) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-snex	⊢ { 𝐴 } ∈ V

Proof

Step	Hyp	Ref	Expression
1		bj-snexg	⊢ ( 𝐴 ∈ V → { 𝐴 } ∈ V )
2		snprc	⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
3	2	biimpi	⊢ ( ¬ 𝐴 ∈ V → { 𝐴 } = ∅ )
4		0ex	⊢ ∅ ∈ V
5	3 4	eqeltrdi	⊢ ( ¬ 𝐴 ∈ V → { 𝐴 } ∈ V )
6	1 5	pm2.61i	⊢ { 𝐴 } ∈ V