Description: Restricted existential quantification implies its restriction is nonempty. (Contributed by Szymon Jaroszewicz, 3-Apr-2007) Avoid df-clel , ax-8 . (Revised by Gino Giotto, 2-Sep-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | rexn0 | |- ( E. x e. A ph -> A =/= (/) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | dfrex2 | |- ( E. x e. A ph <-> -. A. x e. A -. ph ) |
|
| 2 | rzal | |- ( A = (/) -> A. x e. A -. ph ) |
|
| 3 | 2 | con3i | |- ( -. A. x e. A -. ph -> -. A = (/) ) |
| 4 | 1 3 | sylbi | |- ( E. x e. A ph -> -. A = (/) ) |
| 5 | 4 | neqned | |- ( E. x e. A ph -> A =/= (/) ) |