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	|- F/_ x A
Assertion	nfxneg	|- F/_ x -e A

Proof

Step	Hyp	Ref	Expression
1		nfxneg.1	|- F/_ x A
2	1	a1i	|- ( T. -> F/_ x A )
3	2	nfxnegd	|- ( T. -> F/_ x -e A )
4	3	mptru	|- F/_ x -e A