Metamath Proof Explorer


Theorem brab

Description: The law of concretion for a binary relation. (Contributed by NM, 16-Aug-1999)

Ref Expression
Hypotheses opelopab.1
|- A e. _V
opelopab.2
|- B e. _V
opelopab.3
|- ( x = A -> ( ph <-> ps ) )
opelopab.4
|- ( y = B -> ( ps <-> ch ) )
brab.5
|- R = { <. x , y >. | ph }
Assertion brab
|- ( A R B <-> ch )

Proof

Step Hyp Ref Expression
1 opelopab.1
 |-  A e. _V
2 opelopab.2
 |-  B e. _V
3 opelopab.3
 |-  ( x = A -> ( ph <-> ps ) )
4 opelopab.4
 |-  ( y = B -> ( ps <-> ch ) )
5 brab.5
 |-  R = { <. x , y >. | ph }
6 3 4 5 brabg
 |-  ( ( A e. _V /\ B e. _V ) -> ( A R B <-> ch ) )
7 1 2 6 mp2an
 |-  ( A R B <-> ch )