Description: The setvar x is not free in A. x ph . (Contributed by Mario Carneiro, 11-Aug-2016) df-nf changed. (Revised by Wolf Lammen, 11-Sep-2021) Remove dependency on ax-12 . (Revised by Wolf Lammen, 12-Oct-2021)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nfa1 | |- F/ x A. x ph |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | alex | |- ( A. x ph <-> -. E. x -. ph ) |
|
| 2 | nfe1 | |- F/ x E. x -. ph |
|
| 3 | 2 | nfn | |- F/ x -. E. x -. ph |
| 4 | 1 3 | nfxfr | |- F/ x A. x ph |