![]() |
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 1926. See also the dual pair alnex 1882 / exnal 1927. 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 1880 | . 2 wff ∃𝑥𝜑 |
4 | 1 | wn 3 | . . . 4 wff ¬ 𝜑 |
5 | 4, 2 | wal 1656 | . . 3 wff ∀𝑥 ¬ 𝜑 |
6 | 5 | wn 3 | . 2 wff ¬ ∀𝑥 ¬ 𝜑 |
7 | 3, 6 | wb 198 | 1 wff (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑) |
Colors of variables: wff setvar class |
This definition is referenced by: alnex 1882 eximal 1883 2nalexn 1928 2exnaln 1929 19.43OLD 1988 speimfw 2065 speimfwALT 2066 spimfw 2067 ax6ev 2079 cbvexvw 2146 hbe1w 2152 hbe1 2196 hbe1a 2197 axc16nf 2295 nfex 2358 nfexd 2363 cbvexv1 2370 ax6 2405 drex1 2463 nfexd2 2468 sbex 2598 eujustALT 2644 spcimegf 3505 spcegf 3507 spcimedv 3510 neq0f 4157 n0el 4170 ax6vsep 5010 axnulALT 5012 axpownd 9739 gchi 9762 ballotlem2 31097 axextprim 32123 axrepprim 32124 axunprim 32125 axpowprim 32126 axinfprim 32128 axacprim 32129 distel 32248 bj-axtd 33108 bj-modald 33197 bj-modalbe 33214 bj-hbext 33236 bj-cbvexdv 33270 bj-drex1v 33283 gneispace 39273 pm10.252 39401 hbexgVD 39961 elsetrecslem 43341 |
Copyright terms: Public domain | W3C validator |