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 1782 / 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 1780 | . 2 wff ∃𝑥𝜑 |
4 | 1 | wn 3 | . . . 4 wff ¬ 𝜑 |
5 | 4, 2 | wal 1535 | . . 3 wff ∀𝑥 ¬ 𝜑 |
6 | 5 | wn 3 | . 2 wff ¬ ∀𝑥 ¬ 𝜑 |
7 | 3, 6 | wb 208 | 1 wff (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑) |
Colors of variables: wff setvar class |
This definition is referenced by: alnex 1782 eximal 1783 2nalexn 1828 2exnaln 1829 19.43OLD 1884 speimfw 1966 speimfwALT 1967 spimfw 1968 ax6ev 1972 cbvexvw 2044 hbe1w 2055 hbe1 2147 hbe1a 2148 sbex 2288 nfex 2343 nfexd 2348 cbvexv1 2362 drex1v 2388 ax6 2402 drex1 2463 nfexd2 2468 eujustALT 2657 spcimegf 3589 spcegf 3591 spcimedv 3594 neq0f 4306 n0el 4321 ax6vsep 5207 axnulALT 5208 axpownd 10023 gchi 10046 ballotlem2 31746 axextprim 32927 axrepprim 32928 axunprim 32929 axpowprim 32930 axinfprim 32932 axacprim 32933 distel 33048 bj-axtd 33928 bj-eximALT 33974 bj-modald 34006 bj-modalbe 34022 bj-hbext 34044 bj-cbvexdv 34122 bj-nfexd 34433 sn-dtru 39160 gneispace 40533 pm10.252 40742 hbexgVD 41289 elsetrecslem 44850 |
Copyright terms: Public domain | W3C validator |