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 ∈ A B ∈ V → C ∈ ran ⁡ F ↔ ∃ x ∈ A C = B

Proof

Step Hyp Ref Expression
1 rnmpt.1 ⊢ F = x ∈ A ⟼ B
2 1 rnmpt ⊢ ran ⁡ F = y | ∃ x ∈ A y = B
3 2 eleq2i ⊢ C ∈ ran ⁡ F ↔ C ∈ y | ∃ x ∈ A y = B
4 r19.29 ⊢ ∀ x ∈ A B ∈ V ∧ ∃ x ∈ A C = B → ∃ x ∈ A B ∈ 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 ∈ A B ∈ V ∧ C = B → C ∈ V
9 4 8 syl ⊢ ∀ x ∈ A B ∈ V ∧ ∃ x ∈ A C = B → C ∈ V
10 9 ex ⊢ ∀ x ∈ A B ∈ V → ∃ x ∈ A C = B → C ∈ V
11 eqeq1 ⊢ y = C → y = B ↔ C = B
12 11 rexbidv ⊢ y = C → ∃ x ∈ A y = B ↔ ∃ x ∈ A C = B
13 12 elab3g ⊢ ∃ x ∈ A C = B → C ∈ V → C ∈ y | ∃ x ∈ A y = B ↔ ∃ x ∈ A C = B
14 10 13 syl ⊢ ∀ x ∈ A B ∈ V → C ∈ y | ∃ x ∈ A y = B ↔ ∃ x ∈ A C = B
15 3 14 syl5bb ⊢ ∀ x ∈ A B ∈ V → C ∈ ran ⁡ F ↔ ∃ x ∈ A C = B