Metamath Proof Explorer


Theorem brtpid2

Description: A binary relation involving unordered triples. (Contributed by Scott Fenton, 7-Jun-2016)

Ref Expression
Assertion brtpid2
|- A { C , <. A , B >. , D } B

Proof

Step Hyp Ref Expression
1 opex
 |-  <. A , B >. e. _V
2 1 tpid2
 |-  <. A , B >. e. { C , <. A , B >. , D }
3 df-br
 |-  ( A { C , <. A , B >. , D } B <-> <. A , B >. e. { C , <. A , B >. , D } )
4 2 3 mpbir
 |-  A { C , <. A , B >. , D } B