Theorem ofreq

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

	Ref	Expression
Assertion	ofreq	|- ( R = S -> oR R = oR S )

Proof

Step	Hyp	Ref	Expression
1		breq	|- ( R = S -> ( ( f ` x ) R ( g ` x ) <-> ( f ` x ) S ( g ` x ) ) )
2	1	ralbidv	|- ( R = S -> ( A. x e. ( dom f i^i dom g ) ( f ` x ) R ( g ` x ) <-> A. x e. ( dom f i^i dom g ) ( f ` x ) S ( g ` x ) ) )
3	2	opabbidv	|- ( R = S -> { <. f , g >. | A. x e. ( dom f i^i dom g ) ( f ` x ) R ( g ` x ) } = { <. f , g >. | A. x e. ( dom f i^i dom g ) ( f ` x ) S ( g ` x ) } )
4		df-ofr	|- oR R = { <. f , g >. | A. x e. ( dom f i^i dom g ) ( f ` x ) R ( g ` x ) }
5		df-ofr	|- oR S = { <. f , g >. | A. x e. ( dom f i^i dom g ) ( f ` x ) S ( g ` x ) }
6	3 4 5	3eqtr4g	|- ( R = S -> oR R = oR S )