Theorem ovelrn

Description: A member of an operation's range is a value of the operation. (Contributed by NM, 7-Feb-2007) (Revised by Mario Carneiro, 30-Jan-2014)

	Ref	Expression
Assertion	ovelrn	|- ( F Fn ( A X. B ) -> ( C e. ran F <-> E. x e. A E. y e. B C = ( x F y ) ) )

Proof

Step	Hyp	Ref	Expression
1		fnrnov	|- ( F Fn ( A X. B ) -> ran F = { z | E. x e. A E. y e. B z = ( x F y ) } )
2	1	eleq2d	|- ( F Fn ( A X. B ) -> ( C e. ran F <-> C e. { z | E. x e. A E. y e. B z = ( x F y ) } ) )
3		ovex	|- ( x F y ) e. _V
4		eleq1	|- ( C = ( x F y ) -> ( C e. _V <-> ( x F y ) e. _V ) )
5	3 4	mpbiri	|- ( C = ( x F y ) -> C e. _V )
6	5	rexlimivw	|- ( E. y e. B C = ( x F y ) -> C e. _V )
7	6	rexlimivw	|- ( E. x e. A E. y e. B C = ( x F y ) -> C e. _V )
8		eqeq1	|- ( z = C -> ( z = ( x F y ) <-> C = ( x F y ) ) )
9	8	2rexbidv	|- ( z = C -> ( E. x e. A E. y e. B z = ( x F y ) <-> E. x e. A E. y e. B C = ( x F y ) ) )
10	7 9	elab3	|- ( C e. { z | E. x e. A E. y e. B z = ( x F y ) } <-> E. x e. A E. y e. B C = ( x F y ) )
11	2 10	bitrdi	|- ( F Fn ( A X. B ) -> ( C e. ran F <-> E. x e. A E. y e. B C = ( x F y ) ) )