Description: Equality theorem for singletons. Part of Exercise 4 of TakeutiZaring p. 15. (Contributed by NM, 21Jun1993)
Ref  Expression  

Assertion  sneq   ( A = B > { A } = { B } ) 
Step  Hyp  Ref  Expression 

1  eqeq2   ( A = B > ( x = A <> x = B ) ) 

2  1  abbidv   ( A = B > { x  x = A } = { x  x = B } ) 
3  dfsn   { A } = { x  x = A } 

4  dfsn   { B } = { x  x = B } 

5  2 3 4  3eqtr4g   ( A = B > { A } = { B } ) 