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 ) |
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 ) |