Theorem nfxnegd

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

	Ref	Expression
Hypothesis	nfxnegd.1	|- ( ph -> F/_ x A )
Assertion	nfxnegd	|- ( ph -> F/_ x -e A )

Proof

Step	Hyp	Ref	Expression
1		nfxnegd.1	|- ( ph -> F/_ x A )
2		df-xneg	|- -e A = if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) )
3		nfcvd	|- ( ph -> F/_ x +oo )
4	1 3	nfeqd	|- ( ph -> F/ x A = +oo )
5		nfcvd	|- ( ph -> F/_ x -oo )
6	1 5	nfeqd	|- ( ph -> F/ x A = -oo )
7	1	nfnegd	|- ( ph -> F/_ x -u A )
8	6 3 7	nfifd	|- ( ph -> F/_ x if ( A = -oo , +oo , -u A ) )
9	4 5 8	nfifd	|- ( ph -> F/_ x if ( A = +oo , -oo , if ( A = -oo , +oo , -u A ) ) )
10	2 9	nfcxfrd	|- ( ph -> F/_ x -e A )