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