Theorem ofreq

Description: Equality theorem for function relation. (Contributed by Mario Carneiro, 28-Jul-2014)

	Ref	Expression
Assertion	ofreq	$$⊢R=S\to {\circ }_{r}R={\circ }_{r}S$$

Proof

Step	Hyp	Ref	Expression
1		breq	$$⊢R=S\to \left(f\left(x\right)Rg\left(x\right)\leftrightarrow f\left(x\right)Sg\left(x\right)\right)$$
2	1	ralbidv	$$⊢R=S\to \left(\forall x\in \left(\mathrm{dom}f\cap \mathrm{dom}g\right)f\left(x\right)Rg\left(x\right)\leftrightarrow \forall x\in \left(\mathrm{dom}f\cap \mathrm{dom}g\right)f\left(x\right)Sg\left(x\right)\right)$$
3	2	opabbidv	$$⊢R=S\to \left\{⟨f,g⟩|\forall x\in \left(\mathrm{dom}f\cap \mathrm{dom}g\right)f\left(x\right)Rg\left(x\right)\right\}=\left\{⟨f,g⟩|\forall x\in \left(\mathrm{dom}f\cap \mathrm{dom}g\right)f\left(x\right)Sg\left(x\right)\right\}$$
4		df-ofr	$$⊢{\circ }_{r}R=\left\{⟨f,g⟩|\forall x\in \left(\mathrm{dom}f\cap \mathrm{dom}g\right)f\left(x\right)Rg\left(x\right)\right\}$$
5		df-ofr	$$⊢{\circ }_{r}S=\left\{⟨f,g⟩|\forall x\in \left(\mathrm{dom}f\cap \mathrm{dom}g\right)f\left(x\right)Sg\left(x\right)\right\}$$
6	3 4 5	3eqtr4g	$$⊢R=S\to {\circ }_{r}R={\circ }_{r}S$$