Metamath Proof Explorer

Theorem tpidm12

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

Ref Expression
Assertion tpidm12 
|- { A , A , B } = { A , B }

Proof

Step Hyp Ref Expression
1 dfsn2 
 |-  { A } = { A , A }
2 1 uneq1i 
 |-  ( { A } u. { B } ) = ( { A , A } u. { B } )
3 df-pr 
 |-  { A , B } = ( { A } u. { B } )
4 df-tp 
 |-  { A , A , B } = ( { A , A } u. { B } )
5 2 3 4 3eqtr4ri 
 |-  { A , A , B } = { A , B }