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 1782
Description: Define existential quantification. 𝑥𝜑 means "there exists at least one set 𝑥 such that 𝜑 is true". Dual of alex 1827. See also the dual pair alnex 1783 / exnal 1828. 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 1781 . 2 wff 𝑥𝜑
41wn 3 . . . 4 wff ¬ 𝜑
54, 2wal 1536 . . 3 wff 𝑥 ¬ 𝜑
65wn 3 . 2 wff ¬ ∀𝑥 ¬ 𝜑
73, 6wb 209 1 wff (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
Colors of variables: wff setvar class
This definition is referenced by:  alnex  1783  eximal  1784  2nalexn  1829  2exnaln  1830  19.43OLD  1885  speimfw  1967  speimfwALT  1968  spimfw  1969  ax6ev  1973  cbvexvw  2045  hbe1w  2056  hbe1  2148  hbe1a  2149  sbex  2290  nfex  2345  nfexd  2350  cbvexv1  2364  drex1v  2390  ax6  2404  drex1  2465  nfexd2  2470  eujustALT  2658  spcimegf  3574  spcegf  3576  spcimedv  3579  neq0f  4287  n0el  4302  ax6vsep  5188  axnulALT  5189  axpownd  10008  gchi  10031  ballotlem2  31764  axextprim  32945  axrepprim  32946  axunprim  32947  axpowprim  32948  axinfprim  32950  axacprim  32951  distel  33066  bj-axtd  33946  bj-eximALT  33992  bj-modald  34024  bj-modalbe  34040  bj-hbext  34062  bj-cbvexdv  34141  bj-nfexd  34458  sn-dtru  39262  gneispace  40672  pm10.252  40901  hbexgVD  41448  elsetrecslem  45058
  Copyright terms: Public domain W3C validator