Description: Consequence of the definition of not-free. (Contributed by Mario Carneiro, 11-Aug-2016) (Proof shortened by Wolf Lammen, 15-Mar-2023)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | nf5ri.1 | |- F/ x ph |
|
| Assertion | nf5ri | |- ( ph -> A. x ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nf5ri.1 | |- F/ x ph |
|
| 2 | 1 | nfri | |- ( E. x ph -> A. x ph ) |
| 3 | 2 | 19.23bi | |- ( ph -> A. x ph ) |