Metamath Proof Explorer

Theorem brtpid3

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

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

Proof

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