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∈A,y∈B⟼C
elrnmpo.1 ⊢C∈V
Assertion elrnmpo ⊢D∈ran⁡F↔∃x∈A∃y∈BD=C

Proof

Step Hyp Ref Expression
1 rngop.1 ⊢F=x∈A,y∈B⟼C
2 elrnmpo.1 ⊢C∈V
3 1 rnmpo ⊢ran⁡F=z|∃x∈A∃y∈Bz=C
4 3 eleq2i ⊢D∈ran⁡F↔D∈z|∃x∈A∃y∈Bz=C
5 eleq1 ⊢D=C→D∈V↔C∈V
6 2 5 mpbiri ⊢D=C→D∈V
7 6 rexlimivw ⊢∃y∈BD=C→D∈V
8 7 rexlimivw ⊢∃x∈A∃y∈BD=C→D∈V
9 eqeq1 ⊢z=D→z=C↔D=C
10 9 2rexbidv ⊢z=D→∃x∈A∃y∈Bz=C↔∃x∈A∃y∈BD=C
11 8 10 elab3 ⊢D∈z|∃x∈A∃y∈Bz=C↔∃x∈A∃y∈BD=C
12 4 11 bitri ⊢D∈ran⁡F↔∃x∈A∃y∈BD=C