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	$$⊢A\in \mathrm{V}\leftrightarrow \left\{A\right\}\in \underset{\_}{\mathrm{Moore}}$$

Proof

Step	Hyp	Ref	Expression
1		bj-snmoore	$$⊢A\in \mathrm{V}\to \left\{A\right\}\in \underset{\_}{\mathrm{Moore}}$$
2		snprc	$$⊢\neg A\in \mathrm{V}\leftrightarrow \left\{A\right\}=\varnothing$$
3	2	biimpi	$$⊢\neg A\in \mathrm{V}\to \left\{A\right\}=\varnothing$$
4		bj-0nmoore	$$⊢\neg \varnothing \in \underset{\_}{\mathrm{Moore}}$$
5	4	a1i	$$⊢\neg A\in \mathrm{V}\to \neg \varnothing \in \underset{\_}{\mathrm{Moore}}$$
6	3 5	eqneltrd	$$⊢\neg A\in \mathrm{V}\to \neg \left\{A\right\}\in \underset{\_}{\mathrm{Moore}}$$
7	6	con4i	$$⊢\left\{A\right\}\in \underset{\_}{\mathrm{Moore}}\to A\in \mathrm{V}$$
8	1 7	impbii	$$⊢A\in \mathrm{V}\leftrightarrow \left\{A\right\}\in \underset{\_}{\mathrm{Moore}}$$