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

Theorem exnal 1921
Description: Existential quantification of negation is equivalent to negation of universal quantification. Dual of alnex 1876. See also the dual pair df-ex 1875 / alex 1920. 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 1920 . 2 (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
21con2bii 348 1 (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 197  wal 1650  wex 1874
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904
This theorem depends on definitions:  df-bi 198  df-ex 1875
This theorem is referenced by:  alexn  1940  exanali  1955  19.35  1976  19.30  1980  nfeqf2  2396  nfeqf2OLD  2397  nabbi  3039  r2exlem  3206  spc3gv  3451  notzfaus  5000  dtru  5008  dvdemo1  5011  dtruALT  5025  eunex  5027  reusv2lem2  5036  dtruALT2  5069  brprcneu  6371  dffv2  6464  zfcndpow  9695  hashfun  13430  nmo  29802  bnj1304  31359  bnj1253  31554  axrepprim  32046  axunprim  32047  axregprim  32049  axinfprim  32050  axacprim  32051  dftr6  32106  brtxpsd  32466  elfuns  32487  dfrdg4  32523  bj-dtru  33248  bj-eunex  33250  bj-dvdemo1  33253  relowlpssretop  33666  clsk3nimkb  39036  vk15.4j  39430  vk15.4jVD  39826  alneu  41896
  Copyright terms: Public domain W3C validator