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 1817. See also the dual pair alnex 1773 / exnal 1818. 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 1771 | . 2 wff ∃𝑥𝜑 |
4 | 1 | wn 3 | . . . 4 wff ¬ 𝜑 |
5 | 4, 2 | wal 1526 | . . 3 wff ∀𝑥 ¬ 𝜑 |
6 | 5 | wn 3 | . 2 wff ¬ ∀𝑥 ¬ 𝜑 |
7 | 3, 6 | wb 207 | 1 wff (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑) |
Colors of variables: wff setvar class |
This definition is referenced by: alnex 1773 eximal 1774 2nalexn 1819 2exnaln 1820 19.43OLD 1875 speimfw 1957 speimfwALT 1958 spimfw 1959 ax6ev 1963 cbvexvw 2035 hbe1w 2046 hbe1 2138 hbe1a 2139 sbex 2280 nfex 2335 nfexd 2340 cbvexv1 2354 drex1v 2381 ax6 2395 drex1 2458 nfexd2 2463 eujustALT 2653 spcimegf 3589 spcegf 3591 spcimedv 3594 neq0f 4305 n0el 4320 ax6vsep 5199 axnulALT 5200 axpownd 10012 gchi 10035 ballotlem2 31646 axextprim 32825 axrepprim 32826 axunprim 32827 axpowprim 32828 axinfprim 32830 axacprim 32831 distel 32946 bj-axtd 33826 bj-eximALT 33872 bj-modald 33904 bj-modalbe 33920 bj-hbext 33942 bj-cbvexdv 34020 bj-nfexd 34323 sn-dtru 38991 gneispace 40364 pm10.252 40573 hbexgVD 41120 elsetrecslem 44699 |
Copyright terms: Public domain | W3C validator |