Step |
Hyp |
Ref |
Expression |
1 |
|
eqeq2 |
⊢ ( 𝑦 = 𝐴 → ( ( 𝑧 + 𝑥 ) = 𝑦 ↔ ( 𝑧 + 𝑥 ) = 𝐴 ) ) |
2 |
1
|
riotabidv |
⊢ ( 𝑦 = 𝐴 → ( ℩ 𝑥 ∈ ℝ ( 𝑧 + 𝑥 ) = 𝑦 ) = ( ℩ 𝑥 ∈ ℝ ( 𝑧 + 𝑥 ) = 𝐴 ) ) |
3 |
|
oveq1 |
⊢ ( 𝑧 = 𝐵 → ( 𝑧 + 𝑥 ) = ( 𝐵 + 𝑥 ) ) |
4 |
3
|
eqeq1d |
⊢ ( 𝑧 = 𝐵 → ( ( 𝑧 + 𝑥 ) = 𝐴 ↔ ( 𝐵 + 𝑥 ) = 𝐴 ) ) |
5 |
4
|
riotabidv |
⊢ ( 𝑧 = 𝐵 → ( ℩ 𝑥 ∈ ℝ ( 𝑧 + 𝑥 ) = 𝐴 ) = ( ℩ 𝑥 ∈ ℝ ( 𝐵 + 𝑥 ) = 𝐴 ) ) |
6 |
|
df-resub |
⊢ −ℝ = ( 𝑦 ∈ ℝ , 𝑧 ∈ ℝ ↦ ( ℩ 𝑥 ∈ ℝ ( 𝑧 + 𝑥 ) = 𝑦 ) ) |
7 |
|
riotaex |
⊢ ( ℩ 𝑥 ∈ ℝ ( 𝐵 + 𝑥 ) = 𝐴 ) ∈ V |
8 |
2 5 6 7
|
ovmpo |
⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 −ℝ 𝐵 ) = ( ℩ 𝑥 ∈ ℝ ( 𝐵 + 𝑥 ) = 𝐴 ) ) |