Theorem nfxneg

Description: Bound-variable hypothesis builder for the negative of an extended real number. (Contributed by Glauco Siliprandi, 2-Jan-2022)

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

Proof

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