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 𝑥 𝐶
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 𝐹 )