Theorem bj-snmooreb

Description: A singleton is a Moore collection, biconditional version. (Contributed by BJ, 9-Dec-2021) (Proof shortened by BJ, 10-Apr-2024)

	Ref	Expression
Assertion	bj-snmooreb	⊢ ( 𝐴 ∈ V ↔ { 𝐴 } ∈ Moore )

Proof

Step	Hyp	Ref	Expression
1		bj-snmoore	⊢ ( 𝐴 ∈ V → { 𝐴 } ∈ Moore )
2		snprc	⊢ ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
3	2	biimpi	⊢ ( ¬ 𝐴 ∈ V → { 𝐴 } = ∅ )
4		bj-0nmoore	⊢ ¬ ∅ ∈ Moore
5	4	a1i	⊢ ( ¬ 𝐴 ∈ V → ¬ ∅ ∈ Moore )
6	3 5	eqneltrd	⊢ ( ¬ 𝐴 ∈ V → ¬ { 𝐴 } ∈ Moore )
7	6	con4i	⊢ ( { 𝐴 } ∈ Moore → 𝐴 ∈ V )
8	1 7	impbii	⊢ ( 𝐴 ∈ V ↔ { 𝐴 } ∈ Moore )