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