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