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 V
2 1 tpid2 A B C A B D
3 df-br A C A B D B A B C A B D
4 2 3 mpbir A C A B D B