Metamath Proof Explorer


Theorem ffnov

Description: An operation maps to a class to which all values belong. (Contributed by NM, 7-Feb-2004)

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

Proof

Step Hyp Ref Expression
1 ffnfv F : A × B C F Fn A × B w A × B F w C
2 fveq2 w = x y F w = F x y
3 df-ov x F y = F x y
4 2 3 syl6eqr 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