Metamath Proof Explorer


Theorem brabsb

Description: The law of concretion in terms of substitutions. (Contributed by NM, 17-Mar-2008)

Ref Expression
Hypothesis brabsb.1
|- R = { <. x , y >. | ph }
Assertion brabsb
|- ( A R B <-> [. A / x ]. [. B / y ]. ph )

Proof

Step Hyp Ref Expression
1 brabsb.1
 |-  R = { <. x , y >. | ph }
2 df-br
 |-  ( A R B <-> <. A , B >. e. R )
3 1 eleq2i
 |-  ( <. A , B >. e. R <-> <. A , B >. e. { <. x , y >. | ph } )
4 opelopabsb
 |-  ( <. A , B >. e. { <. x , y >. | ph } <-> [. A / x ]. [. B / y ]. ph )
5 2 3 4 3bitri
 |-  ( A R B <-> [. A / x ]. [. B / y ]. ph )