Metamath Proof Explorer

Theorem ofeq

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

Ref Expression
Assertion ofeq 
|- ( R = S -> oF R = oF S )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( R = S /\ f e. _V /\ g e. _V ) -> R = S )
2 1 oveqd 
 |-  ( ( R = S /\ f e. _V /\ g e. _V ) -> ( ( f ` x ) R ( g ` x ) ) = ( ( f ` x ) S ( g ` x ) ) )
3 2 mpteq2dv 
 |-  ( ( R = S /\ f e. _V /\ g e. _V ) -> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) = ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) S ( g ` x ) ) ) )
4 3 mpoeq3dva 
 |-  ( R = S -> ( f e. _V , g e. _V |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) ) = ( f e. _V , g e. _V |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) S ( g ` x ) ) ) ) )
5 df-of 
 |-  oF R = ( f e. _V , g e. _V |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) R ( g ` x ) ) ) )
6 df-of 
 |-  oF S = ( f e. _V , g e. _V |-> ( x e. ( dom f i^i dom g ) |-> ( ( f ` x ) S ( g ` x ) ) ) )
7 4 5 6 3eqtr4g 
 |-  ( R = S -> oF R = oF S )