Description: Deduction version of nfneg . (Contributed by NM, 29-Feb-2008) (Revised by Mario Carneiro, 15-Oct-2016)
Ref | Expression | ||
---|---|---|---|
Hypothesis | nfnegd.1 | |- ( ph -> F/_ x A ) |
|
Assertion | nfnegd | |- ( ph -> F/_ x -u A ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfnegd.1 | |- ( ph -> F/_ x A ) |
|
2 | df-neg | |- -u A = ( 0 - A ) |
|
3 | nfcvd | |- ( ph -> F/_ x 0 ) |
|
4 | nfcvd | |- ( ph -> F/_ x - ) |
|
5 | 3 4 1 | nfovd | |- ( ph -> F/_ x ( 0 - A ) ) |
6 | 2 5 | nfcxfrd | |- ( ph -> F/_ x -u A ) |