Theorem fnrnov

Description: The range of an operation expressed as a collection of the operation's values. (Contributed by NM, 29-Oct-2006)

	Ref	Expression
Assertion	fnrnov	|- ( F Fn ( A X. B ) -> ran F = { z | E. x e. A E. y e. B z = ( x F y ) } )

Proof

Step	Hyp	Ref	Expression
1		fnrnfv	|- ( F Fn ( A X. B ) -> ran F = { z | E. w e. ( A X. B ) z = ( F ` w ) } )
2		fveq2	|- ( w = <. x , y >. -> ( F ` w ) = ( F ` <. x , y >. ) )
3		df-ov	|- ( x F y ) = ( F ` <. x , y >. )
4	2 3	eqtr4di	|- ( w = <. x , y >. -> ( F ` w ) = ( x F y ) )
5	4	eqeq2d	|- ( w = <. x , y >. -> ( z = ( F ` w ) <-> z = ( x F y ) ) )
6	5	rexxp	|- ( E. w e. ( A X. B ) z = ( F ` w ) <-> E. x e. A E. y e. B z = ( x F y ) )
7	6	abbii	|- { z | E. w e. ( A X. B ) z = ( F ` w ) } = { z | E. x e. A E. y e. B z = ( x F y ) }
8	1 7	eqtrdi	|- ( F Fn ( A X. B ) -> ran F = { z | E. x e. A E. y e. B z = ( x F y ) } )