Description: Apply the definition of not-free in a context. (Contributed by Mario Carneiro, 11-Aug-2016) df-nf changed. (Revised by Wolf Lammen, 18-Sep-2021) (Proof shortened by Wolf Lammen, 13-Jul-2022)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | nf5dv.1 | |- ( ph -> ( ps -> A. x ps ) ) |
|
| Assertion | nf5dv | |- ( ph -> F/ x ps ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nf5dv.1 | |- ( ph -> ( ps -> A. x ps ) ) |
|
| 2 | ax-5 | |- ( ph -> A. x ph ) |
|
| 3 | 2 1 | nf5dh | |- ( ph -> F/ x ps ) |