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 }