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

Metamath Proof Explorer

Theorem elrnmpo

Description: Membership in the range of an operation class abstraction. (Contributed by NM, 1-Aug-2004) (Revised by Mario Carneiro, 31-Aug-2015)

Ref Expression
Hypotheses rngop.1 
|- F = ( x e. A , y e. B |-> C )
elrnmpo.1 
|- C e. _V
Assertion elrnmpo 
|- ( D e. ran F <-> E. x e. A E. y e. B D = C )

Proof

Step Hyp Ref Expression
1 rngop.1 
 |-  F = ( x e. A , y e. B |-> C )
2 elrnmpo.1 
 |-  C e. _V
3 1 rnmpo 
 |-  ran F = { z | E. x e. A E. y e. B z = C }
4 3 eleq2i 
 |-  ( D e. ran F <-> D e. { z | E. x e. A E. y e. B z = C } )
5 eleq1 
 |-  ( D = C -> ( D e. _V <-> C e. _V ) )
6 2 5 mpbiri 
 |-  ( D = C -> D e. _V )
7 6 rexlimivw 
 |-  ( E. y e. B D = C -> D e. _V )
8 7 rexlimivw 
 |-  ( E. x e. A E. y e. B D = C -> D e. _V )
9 eqeq1 
 |-  ( z = D -> ( z = C <-> D = C ) )
10 9 2rexbidv 
 |-  ( z = D -> ( E. x e. A E. y e. B z = C <-> E. x e. A E. y e. B D = C ) )
11 8 10 elab3 
 |-  ( D e. { z | E. x e. A E. y e. B z = C } <-> E. x e. A E. y e. B D = C )
12 4 11 bitri 
 |-  ( D e. ran F <-> E. x e. A E. y e. B D = C )