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

Definition df-ex 1842
 Description: Define existential quantification. ∃𝑥𝜑 means "there exists at least one set 𝑥 such that 𝜑 is true." 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 1841 . 2 wff 𝑥𝜑
41wn 3 . . . 4 wff ¬ 𝜑
54, 2wal 1618 . . 3 wff 𝑥 ¬ 𝜑
65wn 3 . 2 wff ¬ ∀𝑥 ¬ 𝜑
73, 6wb 196 1 wff (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
 Colors of variables: wff setvar class This definition is referenced by:  alnex  1843  eximal  1844  2nalexn  1892  2exnaln  1893  19.43OLD  1948  speimfw  2030  speimfwALT  2031  spimfw  2032  ax6ev  2044  cbvexvw  2109  hbe1w  2115  hbe1  2158  hbe1a  2159  axc16nf  2272  hbntOLD  2280  hbexOLD  2287  nfex  2289  nfexd  2300  cbvexv1  2309  ax6  2384  cbvex  2405  cbvexv  2408  cbvexd  2411  drex1  2455  nfexd2  2460  sbex  2588  eujustALT  2598  spcimegf  3415  spcegf  3417  spcimedv  3420  neq0f  4057  n0fOLD  4059  n0el  4071  dfnf5  4083  ax6vsep  4925  axnulALT  4927  axpownd  9586  gchi  9609  ballotlem2  30830  axextprim  31856  axrepprim  31857  axunprim  31858  axpowprim  31859  axinfprim  31861  axacprim  31862  distel  31985  bj-axtd  32855  bj-modald  32938  bj-modalbe  32955  bj-hbext  32978  bj-cbvexdv  33013  bj-drex1v  33026  gneispace  38903  pm10.252  39031  hbexgVD  39610  elsetrecslem  42924
 Copyright terms: Public domain W3C validator