Metamath Proof Explorer


Theorem tpidm13

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

Ref Expression
Assertion tpidm13 A B A = A B

Proof

Step Hyp Ref Expression
1 tprot A A B = A B A
2 tpidm12 A A B = A B
3 1 2 eqtr3i A B A = A B