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
|- ( ph -> F/_ x A )
Assertion nfnegd
|- ( ph -> F/_ x -u A )

Proof

Step Hyp Ref Expression
1 nfnegd.1
 |-  ( ph -> F/_ x A )
2 df-neg
 |-  -u A = ( 0 - A )
3 nfcvd
 |-  ( ph -> F/_ x 0 )
4 nfcvd
 |-  ( ph -> F/_ x - )
5 3 4 1 nfovd
 |-  ( ph -> F/_ x ( 0 - A ) )
6 2 5 nfcxfrd
 |-  ( ph -> F/_ x -u A )