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	⊢ Ⅎ 𝑥 𝐶
	elrnmpt1sf.2	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
	elrnmpt1sf.3	⊢ ( 𝑥 = 𝐷 → 𝐵 = 𝐶 )
Assertion	elrnmpt1sf	⊢ ( ( 𝐷 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → 𝐶 ∈ ran 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		elrnmpt1sf.1	⊢ Ⅎ 𝑥 𝐶
2		elrnmpt1sf.2	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
3		elrnmpt1sf.3	⊢ ( 𝑥 = 𝐷 → 𝐵 = 𝐶 )
4		eqid	⊢ 𝐶 = 𝐶
5	1 1	nfeq	⊢ Ⅎ 𝑥 𝐶 = 𝐶
6	3	eqeq2d	⊢ ( 𝑥 = 𝐷 → ( 𝐶 = 𝐵 ↔ 𝐶 = 𝐶 ) )
7	5 6	rspce	⊢ ( ( 𝐷 ∈ 𝐴 ∧ 𝐶 = 𝐶 ) → ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 )
8	4 7	mpan2	⊢ ( 𝐷 ∈ 𝐴 → ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 )
9	1 2	elrnmptf	⊢ ( 𝐶 ∈ 𝑉 → ( 𝐶 ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 ) )
10	9	biimparc	⊢ ( ( ∃ 𝑥 ∈ 𝐴 𝐶 = 𝐵 ∧ 𝐶 ∈ 𝑉 ) → 𝐶 ∈ ran 𝐹 )
11	8 10	sylan	⊢ ( ( 𝐷 ∈ 𝐴 ∧ 𝐶 ∈ 𝑉 ) → 𝐶 ∈ ran 𝐹 )