Metamath Proof Explorer


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 )