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 | ||
fvopabf4g.2 | |||
fvopabf4g.3 | |||
Assertion | fvopabf4g |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fvopabf4g.1 | ||
2 | fvopabf4g.2 | ||
3 | fvopabf4g.3 | ||
4 | elmapg | ||
5 | 4 | ancoms | |
6 | 5 | biimp3ar | |
7 | 2 3 1 | fvmpt | |
8 | 6 7 | syl |