Metamath Proof Explorer


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 V
fvopabf4g.2 x = A B = C
fvopabf4g.3 F = x R D B
Assertion fvopabf4g D X R Y A : D R F A = C

Proof

Step Hyp Ref Expression
1 fvopabf4g.1 C V
2 fvopabf4g.2 x = A B = C
3 fvopabf4g.3 F = x R D B
4 elmapg R Y D X A R D A : D R
5 4 ancoms D X R Y A R D A : D R
6 5 biimp3ar D X R Y A : D R A R D
7 2 3 1 fvmpt A R D F A = C
8 6 7 syl D X R Y A : D R F A = C