| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > df-ex | Structured version Visualization version GIF version | ||
| Description: Define existential quantification. ∃𝑥𝜑 means "there exists at least one set 𝑥 such that 𝜑 is true". Dual of alex 1826. See also the dual pair alnex 1781 / exnal 1827. Definition of [Margaris] p. 49. (Contributed by NM, 10-Jan-1993.) |
| Ref | Expression |
|---|---|
| df-ex | ⊢ (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wph | . . 3 wff 𝜑 | |
| 2 | vx | . . 3 setvar 𝑥 | |
| 3 | 1, 2 | wex 1779 | . 2 wff ∃𝑥𝜑 |
| 4 | 1 | wn 3 | . . . 4 wff ¬ 𝜑 |
| 5 | 4, 2 | wal 1538 | . . 3 wff ∀𝑥 ¬ 𝜑 |
| 6 | 5 | wn 3 | . 2 wff ¬ ∀𝑥 ¬ 𝜑 |
| 7 | 3, 6 | wb 206 | 1 wff (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑) |
| Colors of variables: wff setvar class |
| This definition is referenced by: alnex 1781 eximal 1782 2nalexn 1828 2exnaln 1829 19.43OLD 1883 speimfw 1963 speimfwALT 1964 spimfw 1965 ax6ev 1969 cbvexvw 2036 hbe1w 2048 exexw 2051 hbe1 2143 hbe1a 2144 sbex 2281 nfex 2324 nfexd 2329 drex1v 2374 ax6 2389 drex1 2446 nfexd2 2451 eujustALT 2572 spcimegf 3551 spcegf 3592 spcimedv 3595 rexab 3700 neq0f 4348 neq0 4352 n0el 4364 abn0 4385 ax6vsep 5303 axnulALT 5304 exexneq 5439 axpownd 10641 gchi 10664 ballotlem2 34491 cbvex1v 35088 axextprim 35701 axrepprim 35702 axunprim 35703 axpowprim 35704 axinfprim 35706 axacprim 35707 distel 35804 bj-axtd 36595 bj-eximALT 36642 bj-modald 36674 bj-modalbe 36689 bj-hbext 36711 bj-cbvexdv 36801 bj-nfexd 37139 gneispace 44147 pm10.252 44380 hbexgVD 44926 elsetrecslem 49218 |
| Copyright terms: Public domain | W3C validator |