Metamath Proof Explorer

Theorem sneq

Description: Equality theorem for singletons. Part of Exercise 4 of TakeutiZaring p. 15. (Contributed by NM, 21-Jun-1993)

Ref Expression
Assertion sneq 
|- ( A = B -> { A } = { B } )

Proof

Step Hyp Ref Expression
1 eqeq2 
 |-  ( A = B -> ( x = A <-> x = B ) )
2 1 abbidv 
 |-  ( A = B -> { x | x = A } = { x | x = B } )
3 df-sn 
 |-  { A } = { x | x = A }
4 df-sn 
 |-  { B } = { x | x = B }
5 2 3 4 3eqtr4g 
 |-  ( A = B -> { A } = { B } )