Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. 2
⊢ 𝐶 = 𝐶 |
2 | | fvmptg.1 |
. . . 4
⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) |
3 | 2 | eqeq2d 2632 |
. . 3
⊢ (𝑥 = 𝐴 → (𝑦 = 𝐵 ↔ 𝑦 = 𝐶)) |
4 | | eqeq1 2626 |
. . 3
⊢ (𝑦 = 𝐶 → (𝑦 = 𝐶 ↔ 𝐶 = 𝐶)) |
5 | | moeq 3382 |
. . . 4
⊢
∃*𝑦 𝑦 = 𝐵 |
6 | 5 | a1i 11 |
. . 3
⊢ (𝑥 ∈ 𝐷 → ∃*𝑦 𝑦 = 𝐵) |
7 | | fvmptg.2 |
. . . 4
⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) |
8 | | df-mpt 4730 |
. . . 4
⊢ (𝑥 ∈ 𝐷 ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)} |
9 | 7, 8 | eqtri 2644 |
. . 3
⊢ 𝐹 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)} |
10 | 3, 4, 6, 9 | fvopab3ig 6278 |
. 2
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐶 = 𝐶 → (𝐹‘𝐴) = 𝐶)) |
11 | 1, 10 | mpi 20 |
1
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐹‘𝐴) = 𝐶) |