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 AV
opelopab.2 BV
opelopab.3 x=Aφψ
opelopab.4 y=Bψχ
brab.5 R=xy|φ
Assertion brab ARBχ

Proof

Step Hyp Ref Expression
1 opelopab.1 AV
2 opelopab.2 BV
3 opelopab.3 x=Aφψ
4 opelopab.4 y=Bψχ
5 brab.5 R=xy|φ
6 3 4 5 brabg AVBVARBχ
7 1 2 6 mp2an ARBχ