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 X. B ) --> C <-> ( F Fn ( A X. B ) /\ A. x e. A A. y e. B (( x F y )) e. C ) )

Proof

Step	Hyp	Ref	Expression
1		ffnafv	|- ( F : ( A X. B ) --> C <-> ( F Fn ( A X. B ) /\ A. w e. ( A X. B ) ( F ''' w ) e. 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 ) e. C <-> (( x F y )) e. C ) )
6	5	ralxp	|- ( A. w e. ( A X. B ) ( F ''' w ) e. C <-> A. x e. A A. y e. B (( x F y )) e. C )
7	6	anbi2i	|- ( ( F Fn ( A X. B ) /\ A. w e. ( A X. B ) ( F ''' w ) e. C ) <-> ( F Fn ( A X. B ) /\ A. x e. A A. y e. B (( x F y )) e. C ) )
8	1 7	bitri	|- ( F : ( A X. B ) --> C <-> ( F Fn ( A X. B ) /\ A. x e. A A. y e. B (( x F y )) e. C ) )