This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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