Metamath Proof Explorer

Theorem brtpid1

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

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

Proof

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