Theorem brabsb2

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

	Ref	Expression
Assertion	brabsb2	$$⊢R=\left\{⟨x,y⟩|\phi \right\}\to \left(zRw\leftrightarrow \left[z/x\right]\left[w/y\right]\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		breq	$$⊢R=\left\{⟨x,y⟩|\phi \right\}\to \left(zRw\leftrightarrow z\left\{⟨x,y⟩|\phi \right\}w\right)$$
2		df-br	$$⊢z\left\{⟨x,y⟩|\phi \right\}w\leftrightarrow ⟨z,w⟩\in \left\{⟨x,y⟩|\phi \right\}$$
3	1 2	bitrdi	$$⊢R=\left\{⟨x,y⟩|\phi \right\}\to \left(zRw\leftrightarrow ⟨z,w⟩\in \left\{⟨x,y⟩|\phi \right\}\right)$$
4		vopelopabsb	$$⊢⟨z,w⟩\in \left\{⟨x,y⟩|\phi \right\}\leftrightarrow \left[z/x\right]\left[w/y\right]\phi$$
5	3 4	bitrdi	$$⊢R=\left\{⟨x,y⟩|\phi \right\}\to \left(zRw\leftrightarrow \left[z/x\right]\left[w/y\right]\phi \right)$$