Metamath Proof Explorer

Theorem elrnmpt

Description: The range of a function in maps-to notation. (Contributed by Mario Carneiro, 20-Feb-2015)

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

Proof

Step Hyp Ref Expression
1 rnmpt.1 ⊢ F = x ∈ A ⟼ B
2 eqeq1 ⊢ y = C → y = B ↔ C = B
3 2 rexbidv ⊢ y = C → ∃ x ∈ A y = B ↔ ∃ x ∈ A C = B
4 1 rnmpt ⊢ ran ⁡ F = y | ∃ x ∈ A y = B
5 3 4 elab2g ⊢ C ∈ V → C ∈ ran ⁡ F ↔ ∃ x ∈ A C = B