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 )