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

Theorem exnal 1820
Description: Existential quantification of negation is equivalent to negation of universal quantification. Dual of alnex 1775. See also the dual pair df-ex 1774 / alex 1819. 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 1819 . 2 (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
21con2bii 359 1 (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 207  wal 1528  wex 1773
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803
This theorem depends on definitions:  df-bi 208  df-ex 1774
This theorem is referenced by:  alexn  1838  exanali  1852  19.35  1871  19.30  1875  nfeqf2  2390  nabbi  3126  r2exlem  3307  spc3gv  3609  notzfaus  5259  notzfausOLD  5260  dtru  5268  dvdemo1  5271  dtruALT  5285  eunex  5287  reusv2lem2  5296  dtruALT2  5332  brprcneu  6659  dffv2  6753  zfcndpow  10027  hashfun  13788  nmo  30168  bnj1304  31977  bnj1253  32173  axrepprim  32812  axunprim  32813  axregprim  32815  axinfprim  32816  axacprim  32817  dftr6  32870  brtxpsd  33239  elfuns  33260  dfrdg4  33296  bj-dtru  34023  relowlpssretop  34514  sn-dtru  38976  clsk3nimkb  40255  expandexn  40490  vk15.4j  40727  vk15.4jVD  41113  alneu  43189
  Copyright terms: Public domain W3C validator