Description: Define existential quantification. E. x ph means "there exists at least one set x such that ph is true". Dual of alex . See also the dual pair alnex / exnal . Definition of Margaris p. 49. (Contributed by NM, 10-Jan-1993)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-ex | |- ( E. x ph <-> -. A. x -. ph ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | vx | |- x |
|
| 1 | wph | |- ph |
|
| 2 | 1 0 | wex | |- E. x ph |
| 3 | 1 | wn | |- -. ph |
| 4 | 3 0 | wal | |- A. x -. ph |
| 5 | 4 | wn | |- -. A. x -. ph |
| 6 | 2 5 | wb | |- ( E. x ph <-> -. A. x -. ph ) |