Theorem en1eqsnbi

Description: A set containing an element has exactly one element iff it is a singleton. Formerly part of proof for rngen1zr . (Contributed by FL, 13-Feb-2010) (Revised by AV, 25-Jan-2020)

	Ref	Expression
Assertion	en1eqsnbi	$$⊢A\in B\to \left(B\approx 1_{𝑜}\leftrightarrow B=\left\{A\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		en1eqsn	$$⊢\left(A\in B\wedge B\approx 1_{𝑜}\right)\to B=\left\{A\right\}$$
2	1	ex	$$⊢A\in B\to \left(B\approx 1_{𝑜}\to B=\left\{A\right\}\right)$$
3		ensn1g	$$⊢A\in B\to \left\{A\right\}\approx 1_{𝑜}$$
4		breq1	$$⊢B=\left\{A\right\}\to \left(B\approx 1_{𝑜}\leftrightarrow \left\{A\right\}\approx 1_{𝑜}\right)$$
5	3 4	syl5ibrcom	$$⊢A\in B\to \left(B=\left\{A\right\}\to B\approx 1_{𝑜}\right)$$
6	2 5	impbid	$$⊢A\in B\to \left(B\approx 1_{𝑜}\leftrightarrow B=\left\{A\right\}\right)$$