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 1702
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 1701 . 2 wff 𝑥𝜑
41wn 3 . . . 4 wff ¬ 𝜑
54, 2wal 1478 . . 3 wff 𝑥 ¬ 𝜑
65wn 3 . 2 wff ¬ ∀𝑥 ¬ 𝜑
73, 6wb 196 1 wff (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
Colors of variables: wff setvar class
This definition is referenced by:  alnex  1703  eximal  1704  2nalexn  1752  2exnaln  1753  19.43OLD  1808  speimfw  1873  speimfwALT  1874  spimfw  1875  ax6ev  1887  cbvexvw  1967  hbe1w  1973  hbe1  2018  hbe1a  2019  axc16nf  2133  hbntOLD  2141  hbexOLD  2149  nfex  2151  nfexd  2164  cbvexv1  2175  ax6  2250  cbvex  2271  cbvexv  2274  cbvexd  2277  drex1  2326  nfexd2  2331  sbex  2462  eujustALT  2472  spcimegf  3273  spcegf  3275  spcimedv  3278  neq0f  3902  n0fOLD  3904  dfnf5  3926  ax6vsep  4745  axnulALT  4747  axpownd  9367  gchi  9390  ballotlem2  30328  axextprim  31283  axrepprim  31284  axunprim  31285  axpowprim  31286  axinfprim  31288  axacprim  31289  distel  31407  bj-axtd  32217  bj-modald  32300  bj-modalbe  32317  bj-hbext  32340  bj-cbvexdv  32375  bj-drex1v  32389  n0el  33623  gneispace  37911  pm10.252  38039  hbexgVD  38622  elsetrecslem  41734
  Copyright terms: Public domain W3C validator