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=AA

Proof

Step Hyp Ref Expression
1 df-pr AA=AA
2 unidm AA=A
3 1 2 eqtr2i A=AA