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 ⊢ Ⅎ _ x A
Assertion nfxneg ⊢ Ⅎ _ x − A

Proof

Step Hyp Ref Expression
1 nfxneg.1 ⊢ Ⅎ _ x A
2 1 a1i ⊢ ⊤ → Ⅎ _ x A
3 2 nfxnegd ⊢ ⊤ → Ⅎ _ x − A
4 3 mptru ⊢ Ⅎ _ x − A