Metamath Proof Explorer

Theorem elrnmpt1s

Description: Elementhood in an image set. (Contributed by Mario Carneiro, 12-Sep-2015)

Ref Expression
Hypotheses rnmpt.1 ⊢ F = x ∈ A ⟼ B
elrnmpt1s.1 ⊢ x = D → B = C
Assertion elrnmpt1s ⊢ D ∈ A ∧ C ∈ V → C ∈ ran ⁡ F

Proof

Step Hyp Ref Expression
1 rnmpt.1 ⊢ F = x ∈ A ⟼ B
2 elrnmpt1s.1 ⊢ x = D → B = C
3 eqid ⊢ C = C
4 2 rspceeqv ⊢ D ∈ A ∧ C = C → ∃ x ∈ A C = B
5 3 4 mpan2 ⊢ D ∈ A → ∃ x ∈ A C = B
6 1 elrnmpt ⊢ C ∈ V → C ∈ ran ⁡ F ↔ ∃ x ∈ A C = B
7 6 biimparc ⊢ ∃ x ∈ A C = B ∧ C ∈ V → C ∈ ran ⁡ F
8 5 7 sylan ⊢ D ∈ A ∧ C ∈ V → C ∈ ran ⁡ F