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 1788
Description: Define existential quantification. 𝑥𝜑 means "there exists at least one set 𝑥 such that 𝜑 is true". Dual of alex 1833. See also the dual pair alnex 1789 / exnal 1834. 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 1787 . 2 wff 𝑥𝜑
41wn 3 . . . 4 wff ¬ 𝜑
54, 2wal 1541 . . 3 wff 𝑥 ¬ 𝜑
65wn 3 . 2 wff ¬ ∀𝑥 ¬ 𝜑
73, 6wb 209 1 wff (∃𝑥𝜑 ↔ ¬ ∀𝑥 ¬ 𝜑)
Colors of variables: wff setvar class
This definition is referenced by:  alnex  1789  eximal  1790  2nalexn  1835  2exnaln  1836  19.43OLD  1891  speimfw  1972  speimfwALT  1973  spimfw  1974  ax6ev  1978  cbvexvw  2045  hbe1w  2056  exexw  2059  hbe1  2145  hbe1a  2146  sbex  2284  nfex  2325  nfexd  2330  drex1v  2371  ax6  2385  drex1  2442  nfexd2  2447  eujustALT  2573  spcimegf  3519  spcegf  3521  spcimedv  3524  rexab  3623  neq0f  4272  neq0  4276  n0el  4292  abn0  4311  ax6vsep  5212  axnulALT  5213  axpownd  10242  gchi  10265  ballotlem2  32196  axextprim  33383  axrepprim  33384  axunprim  33385  axpowprim  33386  axinfprim  33388  axacprim  33389  distel  33526  bj-axtd  34544  bj-eximALT  34590  bj-modald  34622  bj-modalbe  34638  bj-hbext  34660  bj-cbvexdv  34750  bj-nfexd  35076  sn-dtru  39946  gneispace  41456  pm10.252  41687  hbexgVD  42234  elsetrecslem  46108
  Copyright terms: Public domain W3C validator