Metamath Proof Explorer

Theorem elrnmptg

Description: Membership in the range of a function. (Contributed by NM, 27-Aug-2007) (Revised by Mario Carneiro, 31-Aug-2015)

Ref Expression
Hypothesis rnmpt.1 ⊢F=x∈A⟼B
Assertion elrnmptg ⊢∀x∈AB∈V→C∈ran⁡F↔∃x∈AC=B

Proof

Step Hyp Ref Expression
1 rnmpt.1 ⊢F=x∈A⟼B
2 1 rnmpt ⊢ran⁡F=y|∃x∈Ay=B
3 2 eleq2i ⊢C∈ran⁡F↔C∈y|∃x∈Ay=B
4 r19.29 ⊢∀x∈AB∈V∧∃x∈AC=B→∃x∈AB∈V∧C=B
5 eleq1 ⊢C=B→C∈V↔B∈V
6 5 biimparc ⊢B∈V∧C=B→C∈V
7 6 elexd ⊢B∈V∧C=B→C∈V
8 7 rexlimivw ⊢∃x∈AB∈V∧C=B→C∈V
9 4 8 syl ⊢∀x∈AB∈V∧∃x∈AC=B→C∈V
10 9 ex ⊢∀x∈AB∈V→∃x∈AC=B→C∈V
11 eqeq1 ⊢y=C→y=B↔C=B
12 11 rexbidv ⊢y=C→∃x∈Ay=B↔∃x∈AC=B
13 12 elab3g ⊢∃x∈AC=B→C∈V→C∈y|∃x∈Ay=B↔∃x∈AC=B
14 10 13 syl ⊢∀x∈AB∈V→C∈y|∃x∈Ay=B↔∃x∈AC=B
15 3 14 bitrid ⊢∀x∈AB∈V→C∈ran⁡F↔∃x∈AC=B