Theorem brabsb2

Description: A closed form of brabsb . (Contributed by Rodolfo Medina, 13-Oct-2010)

	Ref	Expression
Assertion	brabsb2	|- ( R = { <. x , y >. | ph } -> ( z R w <-> [ z / x ] [ w / y ] ph ) )

Proof

Step	Hyp	Ref	Expression
1		breq	|- ( R = { <. x , y >. | ph } -> ( z R w <-> z { <. x , y >. | ph } w ) )
2		df-br	|- ( z { <. x , y >. | ph } w <-> <. z , w >. e. { <. x , y >. | ph } )
3	1 2	bitrdi	|- ( R = { <. x , y >. | ph } -> ( z R w <-> <. z , w >. e. { <. x , y >. | ph } ) )
4		vopelopabsb	|- ( <. z , w >. e. { <. x , y >. | ph } <-> [ z / x ] [ w / y ] ph )
5	3 4	bitrdi	|- ( R = { <. x , y >. | ph } -> ( z R w <-> [ z / x ] [ w / y ] ph ) )