Metamath Proof Explorer


Theorem ffnaov

Description: An operation maps to a class to which all values belong, analogous to ffnov . (Contributed by Alexander van der Vekens, 26-May-2017)

Ref Expression
Assertion ffnaov F : A × B C F Fn A × B x A y B x F y C

Proof

Step Hyp Ref Expression
1 ffnafv F : A × B C F Fn A × B w A × B F ''' w C
2 afveq2 w = x y F ''' w = F ''' x y
3 df-aov x F y = F ''' x y
4 2 3 eqtr4di w = x y F ''' w = x F y
5 4 eleq1d w = x y F ''' w C x F y C
6 5 ralxp w A × B F ''' w C x A y B x F y C
7 6 anbi2i F Fn A × B w A × B F ''' w C F Fn A × B x A y B x F y C
8 1 7 bitri F : A × B C F Fn A × B x A y B x F y C