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 1693
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 1692 . 2 wff 𝑥𝜑
41wn 3 . . . 4 wff ¬ 𝜑
54, 2wal 1466 . . 3 wff 𝑥 ¬ 𝜑
65wn 3 . 2 wff ¬ ∀𝑥 ¬ 𝜑
73, 6wb 191 1 wff (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
Colors of variables: wff setvar class
This definition is referenced by:  alnex  1694  eximal  1695  2nalexn  1731  2exnaln  1732  19.43OLD  1777  speimfw  1824  speimfwALT  1825  spimfw  1826  ax6ev  1838  cbvexvw  1918  hbe1w  1923  hbe1  1967  excomOLD  1978  axc7e  1993  hbnt  2029  hbex  2081  nfexd  2087  cbvexv1  2117  ax6  2142  cbvex  2162  cbvexd  2166  drex1  2210  nfexd2  2215  sbex  2346  eujustALT  2356  spcimegf  3149  spcegf  3151  spcimedv  3154  n0f  3766  eq0  3773  dfnf5  3787  ax6vsep  4562  axnulALT  4564  axpownd  9111  gchi  9134  ballotlem2  29475  axextprim  30480  axrepprim  30481  axunprim  30482  axpowprim  30483  axinfprim  30485  axacprim  30486  distel  30601  bj-axtd  31361  bj-nalnaleximiOLD  31404  bj-modald  31454  bj-modalbe  31466  bj-hbext  31489  bj-cbvexdv  31524  bj-drex1v  31540  wl-dveeq12  32088  n0el  32666  gneispace  36930  pm10.252  37067  hbexgVD  37651
  Copyright terms: Public domain W3C validator