MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  exnal Structured version   Visualization version   GIF version

Theorem exnal 1833
Description: Existential quantification of negation is equivalent to negation of universal quantification. Dual of alnex 1788. See also the dual pair df-ex 1787 / alex 1832. Theorem 19.14 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
Assertion
Ref Expression
exnal (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)

Proof of Theorem exnal
StepHypRef Expression
1 alex 1832 . 2 (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
21con2bii 361 1 (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 209  wal 1540  wex 1786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816
This theorem depends on definitions:  df-bi 210  df-ex 1787
This theorem is referenced by:  alexn  1851  nfnbi  1861  exanali  1866  19.35  1884  19.30  1888  nfeqf2  2377  nabbi  3036  r2exlem  3212  spc3gv  3508  vn0  4227  notzfaus  5228  notzfausOLD  5229  dtru  5237  dvdemo1  5240  dtruALT  5255  eunex  5257  reusv2lem2  5266  dtruALT2  5302  brprcneu  6665  fvprc  6666  dffv2  6763  zfcndpow  10116  hashfun  13890  nmo  30412  bnj1304  32370  bnj1253  32568  axrepprim  33214  axunprim  33215  axregprim  33217  axinfprim  33218  axacprim  33219  dftr6  33289  brtxpsd  33834  elfuns  33855  dfrdg4  33891  bj-dtru  34630  relowlpssretop  35158  sn-dtru  39779  clsk3nimkb  41196  expandexn  41449  vk15.4j  41686  vk15.4jVD  42072  alneu  44149
  Copyright terms: Public domain W3C validator