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