Theorem nfxnegd

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

	Ref	Expression
Hypothesis	nfxnegd.1	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
Assertion	nfxnegd	$$⊢\phi \to \underset{\_}{Ⅎ}x\left(-A\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfxnegd.1	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
2		df-xneg	$$⊢-A=if\left(A=\mathrm{+\infty },\mathrm{-\infty },if\left(A=\mathrm{-\infty },\mathrm{+\infty },-A\right)\right)$$
3		nfcvd	$$⊢\phi \to \underset{\_}{Ⅎ}x\mathrm{+\infty }$$
4	1 3	nfeqd	$$⊢\phi \to ℲxA=\mathrm{+\infty }$$
5		nfcvd	$$⊢\phi \to \underset{\_}{Ⅎ}x\mathrm{-\infty }$$
6	1 5	nfeqd	$$⊢\phi \to ℲxA=\mathrm{-\infty }$$
7	1	nfnegd	$$⊢\phi \to \underset{\_}{Ⅎ}x\left(-A\right)$$
8	6 3 7	nfifd	$$⊢\phi \to \underset{\_}{Ⅎ}xif\left(A=\mathrm{-\infty },\mathrm{+\infty },-A\right)$$
9	4 5 8	nfifd	$$⊢\phi \to \underset{\_}{Ⅎ}xif\left(A=\mathrm{+\infty },\mathrm{-\infty },if\left(A=\mathrm{-\infty },\mathrm{+\infty },-A\right)\right)$$
10	2 9	nfcxfrd	$$⊢\phi \to \underset{\_}{Ⅎ}x\left(-A\right)$$