Metamath Proof Explorer


Theorem tpidm

Description: Unordered triple { A , A , A } is just an overlong way to write { A } . (Contributed by David A. Wheeler, 10-May-2015)

Ref Expression
Assertion tpidm A A A = A

Proof

Step Hyp Ref Expression
1 tpidm12 A A A = A A
2 dfsn2 A = A A
3 1 2 eqtr4i A A A = A