Theorem fvopabf4g

Description: Function value of an operator abstraction whose domain is a set of functions with given domain and range. (Contributed by Jeff Madsen, 1-Dec-2009) (Revised by Mario Carneiro, 12-Sep-2015)

	Ref	Expression
Hypotheses	fvopabf4g.1	|- C e. _V
	fvopabf4g.2	|- ( x = A -> B = C )
	fvopabf4g.3	|- F = ( x e. ( R ^m D ) |-> B )
Assertion	fvopabf4g	|- ( ( D e. X /\ R e. Y /\ A : D --> R ) -> ( F ` A ) = C )

Proof

Step	Hyp	Ref	Expression
1		fvopabf4g.1	|- C e. _V
2		fvopabf4g.2	|- ( x = A -> B = C )
3		fvopabf4g.3	|- F = ( x e. ( R ^m D ) |-> B )
4		elmapg	|- ( ( R e. Y /\ D e. X ) -> ( A e. ( R ^m D ) <-> A : D --> R ) )
5	4	ancoms	|- ( ( D e. X /\ R e. Y ) -> ( A e. ( R ^m D ) <-> A : D --> R ) )
6	5	biimp3ar	|- ( ( D e. X /\ R e. Y /\ A : D --> R ) -> A e. ( R ^m D ) )
7	2 3 1	fvmpt	|- ( A e. ( R ^m D ) -> ( F ` A ) = C )
8	6 7	syl	|- ( ( D e. X /\ R e. Y /\ A : D --> R ) -> ( F ` A ) = C )