Theorem bj-elsnb

Description: Biconditional version of elsng . (Contributed by BJ, 18-Nov-2023)

	Ref	Expression
Assertion	bj-elsnb	$$⊢A\in \left\{B\right\}\leftrightarrow \left(A\in \mathrm{V}\wedge A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		elex	$$⊢A\in \left\{B\right\}\to A\in \mathrm{V}$$
2		elsng	$$⊢A\in \mathrm{V}\to \left(A\in \left\{B\right\}\leftrightarrow A=B\right)$$
3	1 2	biadanii	$$⊢A\in \left\{B\right\}\leftrightarrow \left(A\in \mathrm{V}\wedge A=B\right)$$