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

Metamath Proof Explorer

Theorem nfxnegd

Description: Deduction version of nfxneg . (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypothesis nfxnegd.1 ⊢ φ → Ⅎ _ x A
Assertion nfxnegd ⊢ φ → Ⅎ _ x − A

Proof

Step Hyp Ref Expression
1 nfxnegd.1 ⊢ φ → Ⅎ _ x A
2 df-xneg ⊢ − A = if A = +∞ −∞ if A = −∞ +∞ − A
3 nfcvd ⊢ φ → Ⅎ _ x +∞
4 1 3 nfeqd ⊢ φ → Ⅎ x A = +∞
5 nfcvd ⊢ φ → Ⅎ _ x −∞
6 1 5 nfeqd ⊢ φ → Ⅎ x A = −∞
7 1 nfnegd ⊢ φ → Ⅎ _ x − A
8 6 3 7 nfifd ⊢ φ → Ⅎ _ x if A = −∞ +∞ − A
9 4 5 8 nfifd ⊢ φ → Ⅎ _ x if A = +∞ −∞ if A = −∞ +∞ − A
10 2 9 nfcxfrd ⊢ φ → Ⅎ _ x − A