![]() |
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 1820. See also the dual pair alnex 1775 / exnal 1821. 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 1773 | . 2 wff ∃𝑥𝜑 |
4 | 1 | wn 3 | . . . 4 wff ¬ 𝜑 |
5 | 4, 2 | wal 1531 | . . 3 wff ∀𝑥 ¬ 𝜑 |
6 | 5 | wn 3 | . 2 wff ¬ ∀𝑥 ¬ 𝜑 |
7 | 3, 6 | wb 205 | 1 wff (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑) |
Colors of variables: wff setvar class |
This definition is referenced by: alnex 1775 eximal 1776 2nalexn 1822 2exnaln 1823 19.43OLD 1878 speimfw 1959 speimfwALT 1960 spimfw 1961 ax6ev 1965 cbvexvw 2032 hbe1w 2043 exexw 2046 hbe1 2131 hbe1a 2132 sbex 2270 nfex 2312 nfexd 2317 drex1v 2362 ax6 2377 drex1 2434 nfexd2 2439 eujustALT 2560 spcimegf 3574 spcegf 3576 spcimedv 3579 rexab 3686 neq0f 4341 neq0 4345 n0el 4361 abn0 4382 ax6vsep 5304 axnulALT 5305 exexneq 5436 axpownd 10631 gchi 10654 ballotlem2 34259 axextprim 35446 axrepprim 35447 axunprim 35448 axpowprim 35449 axinfprim 35451 axacprim 35452 distel 35550 bj-axtd 36222 bj-eximALT 36268 bj-modald 36300 bj-modalbe 36316 bj-hbext 36338 bj-cbvexdv 36428 bj-nfexd 36768 nfa1w 42240 gneispace 43711 pm10.252 43945 hbexgVD 44492 elsetrecslem 48321 |
Copyright terms: Public domain | W3C validator |