This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality Unordered and ordered pairs elsn2g
Description: There is exactly one element in a singleton. Exercise 2 of
TakeutiZaring p. 15. This variation requires only that B , rather
than A , be a set. (Contributed by NM , 28-Oct-2003)
Ref
Expression
Assertion
elsn2g ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ { 𝐵 } ↔ 𝐴 = 𝐵 ) )
Proof
Step
Hyp
Ref
Expression
1
elsni ⊢ ( 𝐴 ∈ { 𝐵 } → 𝐴 = 𝐵 )
2
snidg ⊢ ( 𝐵 ∈ 𝑉 → 𝐵 ∈ { 𝐵 } )
3
eleq1 ⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∈ { 𝐵 } ↔ 𝐵 ∈ { 𝐵 } ) )
4
2 3
syl5ibrcom ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 = 𝐵 → 𝐴 ∈ { 𝐵 } ) )
5
1 4
impbid2 ⊢ ( 𝐵 ∈ 𝑉 → ( 𝐴 ∈ { 𝐵 } ↔ 𝐴 = 𝐵 ) )