Theorem ofceq

Description: Equality theorem for function/constant operation. (Contributed by Thierry Arnoux, 30-Jan-2017)

	Ref	Expression
Assertion	ofceq	|- ( R = S -> oFC R = oFC S )

Proof

Step	Hyp	Ref	Expression
1		oveq	|- ( R = S -> ( ( f ` x ) R c ) = ( ( f ` x ) S c ) )
2	1	mpteq2dv	|- ( R = S -> ( x e. dom f |-> ( ( f ` x ) R c ) ) = ( x e. dom f |-> ( ( f ` x ) S c ) ) )
3	2	mpoeq3dv	|- ( R = S -> ( f e. _V , c e. _V |-> ( x e. dom f |-> ( ( f ` x ) R c ) ) ) = ( f e. _V , c e. _V |-> ( x e. dom f |-> ( ( f ` x ) S c ) ) ) )
4		df-ofc	|- oFC R = ( f e. _V , c e. _V |-> ( x e. dom f |-> ( ( f ` x ) R c ) ) )
5		df-ofc	|- oFC S = ( f e. _V , c e. _V |-> ( x e. dom f |-> ( ( f ` x ) S c ) ) )
6	3 4 5	3eqtr4g	|- ( R = S -> oFC R = oFC S )