**Description:** The setvar x is not free in E. x ph . (Contributed by Mario
Carneiro, 11-Aug-2016)

Ref | Expression | ||
---|---|---|---|

Assertion | nfe1 | $${\u22a2}\u2132{x}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi}$$ |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | hbe1 | $${\u22a2}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi}\to \forall {x}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi}$$ | |

2 | 1 | nf5i | $${\u22a2}\u2132{x}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi}$$ |