This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )