This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )