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

Theorem exnal 1829
Description: Existential quantification of negation is equivalent to negation of universal quantification. Dual of alnex 1784. See also the dual pair df-ex 1783 / alex 1828. 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 1828 . 2 (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
21con2bii 358 1 (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wal 1537  wex 1782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812
This theorem depends on definitions:  df-bi 206  df-ex 1783
This theorem is referenced by:  alexn  1847  nfnbi  1857  exanali  1862  19.35  1880  19.30  1884  nfeqf2  2377  nabbi  3047  r2exlem  3231  spc3gv  3543  vn0  4272  notzfaus  5285  dtruALT2  5293  dvdemo1  5296  dtruALT  5311  eunex  5313  reusv2lem2  5322  dtru  5359  brprcneu  6764  brprcneuALT  6765  dffv2  6863  zfcndpow  10372  hashfun  14152  nmo  30838  bnj1304  32799  bnj1253  32997  axrepprim  33643  axunprim  33644  axregprim  33646  axinfprim  33647  axacprim  33648  dftr6  33718  brtxpsd  34196  elfuns  34217  dfrdg4  34253  bj-dtru  34999  relowlpssretop  35535  sn-dtru  40188  clsk3nimkb  41650  expandexn  41907  vk15.4j  42148  vk15.4jVD  42534  alneu  44616
  Copyright terms: Public domain W3C validator