Metamath Proof Explorer

Theorem dfsn2

Description: Alternate definition of singleton. Definition 5.1 of TakeutiZaring p. 15. (Contributed by NM, 24-Apr-1994)

Ref Expression
Assertion dfsn2 
|- { A } = { A , A }

Proof

Step Hyp Ref Expression
1 df-pr 
 |-  { A , A } = ( { A } u. { A } )
2 unidm 
 |-  ( { A } u. { A } ) = { A }
3 1 2 eqtr2i 
 |-  { A } = { A , A }