Theorem nfxnegd

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

	Ref	Expression
Hypothesis	nfxnegd.1	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
Assertion	nfxnegd	⊢ ( 𝜑 → Ⅎ 𝑥 -𝑒 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		nfxnegd.1	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
2		df-xneg	⊢ -𝑒 𝐴 = if ( 𝐴 = +∞ , -∞ , if ( 𝐴 = -∞ , +∞ , - 𝐴 ) )
3		nfcvd	⊢ ( 𝜑 → Ⅎ 𝑥 +∞ )
4	1 3	nfeqd	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 = +∞ )
5		nfcvd	⊢ ( 𝜑 → Ⅎ 𝑥 -∞ )
6	1 5	nfeqd	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 = -∞ )
7	1	nfnegd	⊢ ( 𝜑 → Ⅎ 𝑥 - 𝐴 )
8	6 3 7	nfifd	⊢ ( 𝜑 → Ⅎ 𝑥 if ( 𝐴 = -∞ , +∞ , - 𝐴 ) )
9	4 5 8	nfifd	⊢ ( 𝜑 → Ⅎ 𝑥 if ( 𝐴 = +∞ , -∞ , if ( 𝐴 = -∞ , +∞ , - 𝐴 ) ) )
10	2 9	nfcxfrd	⊢ ( 𝜑 → Ⅎ 𝑥 -𝑒 𝐴 )