Metamath Proof Explorer

Theorem elrnmptf

Description: The range of a function in maps-to notation. Same as elrnmpt , but using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses elrnmptf.1 ⊢ Ⅎ _ x C
elrnmptf.2 ⊢ F = x ∈ A ⟼ B
Assertion elrnmptf ⊢ C ∈ V → C ∈ ran ⁡ F ↔ ∃ x ∈ A C = B

Proof

Step Hyp Ref Expression
1 elrnmptf.1 ⊢ Ⅎ _ x C
2 elrnmptf.2 ⊢ F = x ∈ A ⟼ B
3 1 nfeq2 ⊢ Ⅎ x y = C
4 eqeq1 ⊢ y = C → y = B ↔ C = B
5 3 4 rexbid ⊢ y = C → ∃ x ∈ A y = B ↔ ∃ x ∈ A C = B
6 2 rnmpt ⊢ ran ⁡ F = y | ∃ x ∈ A y = B
7 5 6 elab2g ⊢ C ∈ V → C ∈ ran ⁡ F ↔ ∃ x ∈ A C = B