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 1695
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 1694 . 2 wff 𝑥𝜑
41wn 3 . . . 4 wff ¬ 𝜑
54, 2wal 1472 . . 3 wff 𝑥 ¬ 𝜑
65wn 3 . 2 wff ¬ ∀𝑥 ¬ 𝜑
73, 6wb 194 1 wff (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
Colors of variables: wff setvar class
This definition is referenced by:  alnex  1696  eximal  1697  2nalexn  1744  2exnaln  1745  19.43OLD  1799  speimfw  1862  speimfwALT  1863  spimfw  1864  ax6ev  1876  cbvexvw  1956  hbe1w  1962  hbe1  2007  hbe1a  2008  axc16nf  2121  hbntOLD  2129  hbexOLD  2137  nfex  2139  nfexd  2152  cbvexv1  2163  ax6  2238  cbvex  2259  cbvexv  2262  cbvexd  2265  drex1  2314  nfexd2  2319  sbex  2450  eujustALT  2460  spcimegf  3259  spcegf  3261  spcimedv  3264  neq0f  3884  n0fOLD  3886  dfnf5  3905  ax6vsep  4707  axnulALT  4709  axpownd  9279  gchi  9302  ballotlem2  29683  axextprim  30638  axrepprim  30639  axunprim  30640  axpowprim  30641  axinfprim  30643  axacprim  30644  distel  30759  bj-axtd  31557  bj-nalnaleximiOLD  31604  bj-modald  31654  bj-modalbe  31671  bj-hbext  31694  bj-cbvexdv  31729  bj-drex1v  31743  wl-nf-nf2  32259  n0el  32960  gneispace  37248  pm10.252  37378  hbexgVD  37960
  Copyright terms: Public domain W3C validator