Theorem elrnmpt1s

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

	Ref	Expression
Hypotheses	rnmpt.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
	elrnmpt1s.1	⊢ ( 𝑥 = 𝐷 → 𝐵 = 𝐶 )
Assertion	elrnmpt1s	⊢ ( ( 𝐷 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → 𝐶 ∈ ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		rnmpt.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2		elrnmpt1s.1	⊢ ( 𝑥 = 𝐷 → 𝐵 = 𝐶 )
3		eqid	⊢ 𝐶 = 𝐶
4	2	rspceeqv	⊢ ( ( 𝐷 ∈ 𝐴 ∧ 𝐶 = 𝐶 ) → ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 )
5	3 4	mpan2	⊢ ( 𝐷 ∈ 𝐴 → ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 )
6	1	elrnmpt	⊢ ( 𝐶 ∈ 𝑉 → ( 𝐶 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 ) )
7	6	biimparc	⊢ ( ( ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 ∧ 𝐶 ∈ 𝑉 ) → 𝐶 ∈ ran 𝐹 )
8	5 7	sylan	⊢ ( ( 𝐷 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → 𝐶 ∈ ran 𝐹 )