Metamath Proof Explorer

Theorem elrnmpt1sf

Description: Elementhood in an image set. Same as elrnmpt1s , but using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses elrnmpt1sf.1 ⊢ Ⅎ _ x C
elrnmpt1sf.2 ⊢ F = x ∈ A ⟼ B
elrnmpt1sf.3 ⊢ x = D → B = C
Assertion elrnmpt1sf ⊢ D ∈ A ∧ C ∈ V → C ∈ ran ⁡ F

Proof

Step Hyp Ref Expression
1 elrnmpt1sf.1 ⊢ Ⅎ _ x C
2 elrnmpt1sf.2 ⊢ F = x ∈ A ⟼ B
3 elrnmpt1sf.3 ⊢ x = D → B = C
4 eqid ⊢ C = C
5 1 1 nfeq ⊢ Ⅎ x C = C
6 3 eqeq2d ⊢ x = D → C = B ↔ C = C
7 5 6 rspce ⊢ D ∈ A ∧ C = C → ∃ x ∈ A C = B
8 4 7 mpan2 ⊢ D ∈ A → ∃ x ∈ A C = B
9 1 2 elrnmptf ⊢ C ∈ V → C ∈ ran ⁡ F ↔ ∃ x ∈ A C = B
10 9 biimparc ⊢ ∃ x ∈ A C = B ∧ C ∈ V → C ∈ ran ⁡ F
11 8 10 sylan ⊢ D ∈ A ∧ C ∈ V → C ∈ ran ⁡ F