Theorem nfneg

Description: Bound-variable hypothesis builder for the negative of a complex number. (Contributed by NM, 12-Jun-2005) (Revised by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Hypothesis	nfneg.1	$$⊢\underset{\_}{Ⅎ}xA$$
Assertion	nfneg	$$⊢\underset{\_}{Ⅎ}x\left(-A\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfneg.1	$$⊢\underset{\_}{Ⅎ}xA$$
2	1	a1i	$$⊢\top \to \underset{\_}{Ⅎ}xA$$
3	2	nfnegd	$$⊢\top \to \underset{\_}{Ⅎ}x\left(-A\right)$$
4	3	mptru	$$⊢\underset{\_}{Ⅎ}x\left(-A\right)$$