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  1733  2exnaln  1734  19.43OLD  1781  speimfw  1826  speimfwALT  1827  spimfw  1828  ax6ev  1840  cbvexvw  1919  hbe1w  1924  hbe1  1968  axc7e  1993  hbnt  2024  hbex  2078  nfexd  2084  cbvexv1  2116  ax6  2142  cbvex  2163  cbvexv  2166  cbvexd  2169  drex1  2219  nfexd2  2224  sbex  2355  eujustALT  2365  spcimegf  3164  spcegf  3166  spcimedv  3169  neq0f  3788  n0fOLD  3790  dfnf5  3809  ax6vsep  4611  axnulALT  4613  axpownd  9177  gchi  9200  ballotlem2  29685  axextprim  30676  axrepprim  30677  axunprim  30678  axpowprim  30679  axinfprim  30681  axacprim  30682  distel  30796  bj-axtd  31586  bj-nalnaleximiOLD  31633  bj-modald  31683  bj-modalbe  31700  bj-hbext  31723  bj-cbvexdv  31758  bj-drex1v  31773  wl-nf-nf2  32310  wl-axc7ea  32317  wl-nfe1  32335  wl-dveeq12  32364  n0el  33039  gneispace  37334  pm10.252  37464  hbexgVD  38046
 Copyright terms: Public domain W3C validator