Metamath Proof Explorer


Theorem nfnegd

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 ( 𝜑 𝑥 - 𝐴 )