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 1696
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 1695 . 2 wff 𝑥𝜑
41wn 3 . . . 4 wff ¬ 𝜑
54, 2wal 1473 . . 3 wff 𝑥 ¬ 𝜑
65wn 3 . 2 wff ¬ ∀𝑥 ¬ 𝜑
73, 6wb 195 1 wff (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
Colors of variables: wff setvar class
This definition is referenced by:  alnex  1697  eximal  1698  2nalexn  1745  2exnaln  1746  19.43OLD  1800  speimfw  1863  speimfwALT  1864  spimfw  1865  ax6ev  1877  cbvexvw  1957  hbe1w  1963  hbe1  2008  hbe1a  2009  axc16nf  2122  hbntOLD  2130  hbexOLD  2138  nfex  2140  nfexd  2153  cbvexv1  2164  ax6  2239  cbvex  2260  cbvexv  2263  cbvexd  2266  drex1  2315  nfexd2  2320  sbex  2451  eujustALT  2461  spcimegf  3260  spcegf  3262  spcimedv  3265  neq0f  3885  n0fOLD  3887  dfnf5  3906  ax6vsep  4713  axnulALT  4715  axpownd  9302  gchi  9325  ballotlem2  29877  axextprim  30832  axrepprim  30833  axunprim  30834  axpowprim  30835  axinfprim  30837  axacprim  30838  distel  30953  bj-axtd  31751  bj-nalnaleximiOLD  31798  bj-modald  31848  bj-modalbe  31865  bj-hbext  31888  bj-cbvexdv  31923  bj-drex1v  31937  wl-nf-nf2  32463  n0el  33164  gneispace  37452  pm10.252  37582  hbexgVD  38164  elsetrecslem  42243
  Copyright terms: Public domain W3C validator