# 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}=\left({x}\in {A},{y}\in {B}⟼{C}\right)$
elrnmpo.1 ${⊢}{C}\in \mathrm{V}$
Assertion elrnmpo ${⊢}{D}\in \mathrm{ran}{F}↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{D}={C}$

### Proof

Step Hyp Ref Expression
1 rngop.1 ${⊢}{F}=\left({x}\in {A},{y}\in {B}⟼{C}\right)$
2 elrnmpo.1 ${⊢}{C}\in \mathrm{V}$
3 1 rnmpo ${⊢}\mathrm{ran}{F}=\left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}={C}\right\}$
4 3 eleq2i ${⊢}{D}\in \mathrm{ran}{F}↔{D}\in \left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}={C}\right\}$
5 eleq1 ${⊢}{D}={C}\to \left({D}\in \mathrm{V}↔{C}\in \mathrm{V}\right)$
6 2 5 mpbiri ${⊢}{D}={C}\to {D}\in \mathrm{V}$
7 6 rexlimivw ${⊢}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{D}={C}\to {D}\in \mathrm{V}$
8 7 rexlimivw ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{D}={C}\to {D}\in \mathrm{V}$
9 eqeq1 ${⊢}{z}={D}\to \left({z}={C}↔{D}={C}\right)$
10 9 2rexbidv ${⊢}{z}={D}\to \left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}={C}↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{D}={C}\right)$
11 8 10 elab3 ${⊢}{D}\in \left\{{z}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{z}={C}\right\}↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{D}={C}$
12 4 11 bitri ${⊢}{D}\in \mathrm{ran}{F}↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}\exists {y}\in {B}\phantom{\rule{.4em}{0ex}}{D}={C}$