MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-ex Structured version   Visualization version   GIF version

Definition df-ex 1772
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.)
Assertion
Ref Expression
df-ex (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)

Detailed syntax breakdown of Definition df-ex
StepHypRef Expression
1 wph . . 3 wff 𝜑
2 vx . . 3 setvar 𝑥
31, 2wex 1771 . 2 wff 𝑥𝜑
41wn 3 . . . 4 wff ¬ 𝜑
54, 2wal 1526 . . 3 wff 𝑥 ¬ 𝜑
65wn 3 . 2 wff ¬ ∀𝑥 ¬ 𝜑
73, 6wb 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