Step |
Hyp |
Ref |
Expression |
1 |
|
fvmptn.1 |
⊢ ( 𝑥 = 𝐷 → 𝐵 = 𝐶 ) |
2 |
|
fvmptn.2 |
⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) |
3 |
1
|
eleq1d |
⊢ ( 𝑥 = 𝐷 → ( 𝐵 ∈ V ↔ 𝐶 ∈ V ) ) |
4 |
2
|
dmmpt |
⊢ dom 𝐹 = { 𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V } |
5 |
3 4
|
elrab2 |
⊢ ( 𝐷 ∈ dom 𝐹 ↔ ( 𝐷 ∈ 𝐴 ∧ 𝐶 ∈ V ) ) |
6 |
1 2
|
fvmptg |
⊢ ( ( 𝐷 ∈ 𝐴 ∧ 𝐶 ∈ V ) → ( 𝐹 ‘ 𝐷 ) = 𝐶 ) |
7 |
|
eqimss |
⊢ ( ( 𝐹 ‘ 𝐷 ) = 𝐶 → ( 𝐹 ‘ 𝐷 ) ⊆ 𝐶 ) |
8 |
6 7
|
syl |
⊢ ( ( 𝐷 ∈ 𝐴 ∧ 𝐶 ∈ V ) → ( 𝐹 ‘ 𝐷 ) ⊆ 𝐶 ) |
9 |
5 8
|
sylbi |
⊢ ( 𝐷 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐷 ) ⊆ 𝐶 ) |
10 |
|
ndmfv |
⊢ ( ¬ 𝐷 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐷 ) = ∅ ) |
11 |
|
0ss |
⊢ ∅ ⊆ 𝐶 |
12 |
10 11
|
eqsstrdi |
⊢ ( ¬ 𝐷 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐷 ) ⊆ 𝐶 ) |
13 |
9 12
|
pm2.61i |
⊢ ( 𝐹 ‘ 𝐷 ) ⊆ 𝐶 |