Metamath Proof Explorer
Description: Deduction version of nfneg . (Contributed by NM, 29-Feb-2008)
(Revised by Mario Carneiro, 15-Oct-2016)
|
|
Ref |
Expression |
|
Hypothesis |
nfnegd.1 |
⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 ) |
|
Assertion |
nfnegd |
⊢ ( 𝜑 → Ⅎ 𝑥 - 𝐴 ) |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
nfnegd.1 |
⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 ) |
2 |
|
df-neg |
⊢ - 𝐴 = ( 0 − 𝐴 ) |
3 |
|
nfcvd |
⊢ ( 𝜑 → Ⅎ 𝑥 0 ) |
4 |
|
nfcvd |
⊢ ( 𝜑 → Ⅎ 𝑥 − ) |
5 |
3 4 1
|
nfovd |
⊢ ( 𝜑 → Ⅎ 𝑥 ( 0 − 𝐴 ) ) |
6 |
2 5
|
nfcxfrd |
⊢ ( 𝜑 → Ⅎ 𝑥 - 𝐴 ) |