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

Definition df-ex 1703
 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 1702 . 2 wff 𝑥𝜑
41wn 3 . . . 4 wff ¬ 𝜑
54, 2wal 1479 . . 3 wff 𝑥 ¬ 𝜑
65wn 3 . 2 wff ¬ ∀𝑥 ¬ 𝜑
73, 6wb 196 1 wff (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
 Colors of variables: wff setvar class This definition is referenced by:  alnex  1704  eximal  1705  2nalexn  1753  2exnaln  1754  19.43OLD  1809  speimfw  1874  speimfwALT  1875  spimfw  1876  ax6ev  1888  cbvexvw  1968  hbe1w  1974  hbe1  2019  hbe1a  2020  axc16nf  2135  hbntOLD  2143  hbexOLD  2150  nfex  2152  nfexd  2165  cbvexv1  2174  ax6  2249  cbvex  2270  cbvexv  2273  cbvexd  2276  drex1  2325  nfexd2  2330  sbex  2461  eujustALT  2471  spcimegf  3282  spcegf  3284  spcimedv  3287  neq0f  3918  n0fOLD  3920  dfnf5  3943  ax6vsep  4776  axnulALT  4778  axpownd  9408  gchi  9431  ballotlem2  30524  axextprim  31552  axrepprim  31553  axunprim  31554  axpowprim  31555  axinfprim  31557  axacprim  31558  distel  31683  bj-axtd  32553  bj-modald  32636  bj-modalbe  32653  bj-hbext  32676  bj-cbvexdv  32711  bj-drex1v  32724  n0el  33965  gneispace  38252  pm10.252  38380  hbexgVD  38962  elsetrecslem  42209
 Copyright terms: Public domain W3C validator