Metamath Proof Explorer


Theorem brabga

Description: The law of concretion for a binary relation. (Contributed by Mario Carneiro, 19-Dec-2013)

Ref Expression
Hypotheses opelopabga.1
|- ( ( x = A /\ y = B ) -> ( ph <-> ps ) )
brabga.2
|- R = { <. x , y >. | ph }
Assertion brabga
|- ( ( A e. V /\ B e. W ) -> ( A R B <-> ps ) )

Proof

Step Hyp Ref Expression
1 opelopabga.1
 |-  ( ( x = A /\ y = B ) -> ( ph <-> ps ) )
2 brabga.2
 |-  R = { <. x , y >. | ph }
3 df-br
 |-  ( A R B <-> <. A , B >. e. R )
4 2 eleq2i
 |-  ( <. A , B >. e. R <-> <. A , B >. e. { <. x , y >. | ph } )
5 3 4 bitri
 |-  ( A R B <-> <. A , B >. e. { <. x , y >. | ph } )
6 1 opelopabga
 |-  ( ( A e. V /\ B e. W ) -> ( <. A , B >. e. { <. x , y >. | ph } <-> ps ) )
7 5 6 bitrid
 |-  ( ( A e. V /\ B e. W ) -> ( A R B <-> ps ) )