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 1833. See also the dual pair alnex 1789 / exnal 1834. 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 1787 | . 2 wff ∃𝑥𝜑 |
4 | 1 | wn 3 | . . . 4 wff ¬ 𝜑 |
5 | 4, 2 | wal 1541 | . . 3 wff ∀𝑥 ¬ 𝜑 |
6 | 5 | wn 3 | . 2 wff ¬ ∀𝑥 ¬ 𝜑 |
7 | 3, 6 | wb 209 | 1 wff (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑) |
Colors of variables: wff setvar class |
This definition is referenced by: alnex 1789 eximal 1790 2nalexn 1835 2exnaln 1836 19.43OLD 1891 speimfw 1972 speimfwALT 1973 spimfw 1974 ax6ev 1978 cbvexvw 2045 hbe1w 2056 exexw 2059 hbe1 2145 hbe1a 2146 sbex 2284 nfex 2325 nfexd 2330 drex1v 2371 ax6 2385 drex1 2442 nfexd2 2447 eujustALT 2573 spcimegf 3519 spcegf 3521 spcimedv 3524 rexab 3623 neq0f 4272 neq0 4276 n0el 4292 abn0 4311 ax6vsep 5212 axnulALT 5213 axpownd 10242 gchi 10265 ballotlem2 32196 axextprim 33383 axrepprim 33384 axunprim 33385 axpowprim 33386 axinfprim 33388 axacprim 33389 distel 33526 bj-axtd 34544 bj-eximALT 34590 bj-modald 34622 bj-modalbe 34638 bj-hbext 34660 bj-cbvexdv 34750 bj-nfexd 35076 sn-dtru 39946 gneispace 41456 pm10.252 41687 hbexgVD 42234 elsetrecslem 46108 |
Copyright terms: Public domain | W3C validator |