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

Metamath Proof Explorer

Theorem ofeqd

Description: Equality theorem for function operation, deduction form. (Contributed by SN, 11-Nov-2024)

Ref Expression
Hypothesis ofeqd.1 
|- ( ph -> R = S )
Assertion ofeqd 
|- ( ph -> oF R = oF S )

Proof

Step Hyp Ref Expression
1 ofeqd.1 
 |-  ( ph -> R = S )
2 1 oveqd 
 |-  ( ph -> ( ( f ` x ) R ( g ` x ) ) = ( ( f ` x ) S ( g ` x ) ) )
3 2 mpteq2dv 
 |-  ( ph -> ( 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 mpoeq3dv 
 |-  ( ph -> ( 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 
 |-  ( ph -> oF R = oF S )