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	⊢ Ⅎ 𝑥 𝐴
Assertion	nfxneg	⊢ Ⅎ 𝑥 -𝑒 𝐴

Proof

Step	Hyp	Ref	Expression
1		nfxneg.1	⊢ Ⅎ 𝑥 𝐴
2	1	a1i	⊢ ( ⊤ → Ⅎ 𝑥 𝐴 )
3	2	nfxnegd	⊢ ( ⊤ → Ⅎ 𝑥 -𝑒 𝐴 )
4	3	mptru	⊢ Ⅎ 𝑥 -𝑒 𝐴