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	⊢ ( 𝐴 ∈ 𝐵 → ( 𝐵 ≈ 1o ↔ 𝐵 = { 𝐴 } ) )

Proof

Step	Hyp	Ref	Expression
1		en1eqsn	⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐵 ≈ 1o ) → 𝐵 = { 𝐴 } )
2	1	ex	⊢ ( 𝐴 ∈ 𝐵 → ( 𝐵 ≈ 1o → 𝐵 = { 𝐴 } ) )
3		ensn1g	⊢ ( 𝐴 ∈ 𝐵 → { 𝐴 } ≈ 1o )
4		breq1	⊢ ( 𝐵 = { 𝐴 } → ( 𝐵 ≈ 1o ↔ { 𝐴 } ≈ 1o ) )
5	3 4	syl5ibrcom	⊢ ( 𝐴 ∈ 𝐵 → ( 𝐵 = { 𝐴 } → 𝐵 ≈ 1o ) )
6	2 5	impbid	⊢ ( 𝐴 ∈ 𝐵 → ( 𝐵 ≈ 1o ↔ 𝐵 = { 𝐴 } ) )