Step |
Hyp |
Ref |
Expression |
1 |
|
riotaneg.1 |
⊢ ( 𝑥 = - 𝑦 → ( 𝜑 ↔ 𝜓 ) ) |
2 |
|
tru |
⊢ ⊤ |
3 |
|
nfriota1 |
⊢ Ⅎ 𝑦 ( ℩ 𝑦 ∈ ℝ 𝜓 ) |
4 |
3
|
nfneg |
⊢ Ⅎ 𝑦 - ( ℩ 𝑦 ∈ ℝ 𝜓 ) |
5 |
|
renegcl |
⊢ ( 𝑦 ∈ ℝ → - 𝑦 ∈ ℝ ) |
6 |
5
|
adantl |
⊢ ( ( ⊤ ∧ 𝑦 ∈ ℝ ) → - 𝑦 ∈ ℝ ) |
7 |
|
simpr |
⊢ ( ( ⊤ ∧ ( ℩ 𝑦 ∈ ℝ 𝜓 ) ∈ ℝ ) → ( ℩ 𝑦 ∈ ℝ 𝜓 ) ∈ ℝ ) |
8 |
7
|
renegcld |
⊢ ( ( ⊤ ∧ ( ℩ 𝑦 ∈ ℝ 𝜓 ) ∈ ℝ ) → - ( ℩ 𝑦 ∈ ℝ 𝜓 ) ∈ ℝ ) |
9 |
|
negeq |
⊢ ( 𝑦 = ( ℩ 𝑦 ∈ ℝ 𝜓 ) → - 𝑦 = - ( ℩ 𝑦 ∈ ℝ 𝜓 ) ) |
10 |
|
renegcl |
⊢ ( 𝑥 ∈ ℝ → - 𝑥 ∈ ℝ ) |
11 |
|
recn |
⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ ) |
12 |
|
recn |
⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℂ ) |
13 |
|
negcon2 |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑥 = - 𝑦 ↔ 𝑦 = - 𝑥 ) ) |
14 |
11 12 13
|
syl2an |
⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 = - 𝑦 ↔ 𝑦 = - 𝑥 ) ) |
15 |
10 14
|
reuhyp |
⊢ ( 𝑥 ∈ ℝ → ∃! 𝑦 ∈ ℝ 𝑥 = - 𝑦 ) |
16 |
15
|
adantl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ ) → ∃! 𝑦 ∈ ℝ 𝑥 = - 𝑦 ) |
17 |
4 6 8 1 9 16
|
riotaxfrd |
⊢ ( ( ⊤ ∧ ∃! 𝑥 ∈ ℝ 𝜑 ) → ( ℩ 𝑥 ∈ ℝ 𝜑 ) = - ( ℩ 𝑦 ∈ ℝ 𝜓 ) ) |
18 |
2 17
|
mpan |
⊢ ( ∃! 𝑥 ∈ ℝ 𝜑 → ( ℩ 𝑥 ∈ ℝ 𝜑 ) = - ( ℩ 𝑦 ∈ ℝ 𝜓 ) ) |