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