Step |
Hyp |
Ref |
Expression |
1 |
|
elex |
⊢ ( 𝐴 ∈ 𝐶 → 𝐴 ∈ V ) |
2 |
|
elex |
⊢ ( 𝐵 ∈ 𝐷 → 𝐵 ∈ V ) |
3 |
|
fveq1 |
⊢ ( 𝑥 = 𝐴 → ( 𝑥 ‘ 𝑣 ) = ( 𝐴 ‘ 𝑣 ) ) |
4 |
|
fveq1 |
⊢ ( 𝑦 = 𝐵 → ( 𝑦 ‘ 𝑣 ) = ( 𝐵 ‘ 𝑣 ) ) |
5 |
3 4
|
oveqan12d |
⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( ( 𝑥 ‘ 𝑣 ) − ( 𝑦 ‘ 𝑣 ) ) = ( ( 𝐴 ‘ 𝑣 ) − ( 𝐵 ‘ 𝑣 ) ) ) |
6 |
5
|
mpteq2dv |
⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑣 ∈ ℝ ↦ ( ( 𝑥 ‘ 𝑣 ) − ( 𝑦 ‘ 𝑣 ) ) ) = ( 𝑣 ∈ ℝ ↦ ( ( 𝐴 ‘ 𝑣 ) − ( 𝐵 ‘ 𝑣 ) ) ) ) |
7 |
|
df-subr |
⊢ -𝑟 = ( 𝑥 ∈ V , 𝑦 ∈ V ↦ ( 𝑣 ∈ ℝ ↦ ( ( 𝑥 ‘ 𝑣 ) − ( 𝑦 ‘ 𝑣 ) ) ) ) |
8 |
|
reex |
⊢ ℝ ∈ V |
9 |
8
|
mptex |
⊢ ( 𝑣 ∈ ℝ ↦ ( ( 𝐴 ‘ 𝑣 ) − ( 𝐵 ‘ 𝑣 ) ) ) ∈ V |
10 |
6 7 9
|
ovmpoa |
⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 -𝑟 𝐵 ) = ( 𝑣 ∈ ℝ ↦ ( ( 𝐴 ‘ 𝑣 ) − ( 𝐵 ‘ 𝑣 ) ) ) ) |
11 |
1 2 10
|
syl2an |
⊢ ( ( 𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷 ) → ( 𝐴 -𝑟 𝐵 ) = ( 𝑣 ∈ ℝ ↦ ( ( 𝐴 ‘ 𝑣 ) − ( 𝐵 ‘ 𝑣 ) ) ) ) |