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

Theorem exnal 1827
Description: Existential quantification of negation is equivalent to negation of universal quantification. Dual of alnex 1781. See also the dual pair df-ex 1780 / alex 1826. 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 1826 . 2 (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
21con2bii 357 1 (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 206  wal 1538  wex 1779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809
This theorem depends on definitions:  df-bi 207  df-ex 1780
This theorem is referenced by:  alexn  1845  nfnbi  1855  exanali  1859  19.35  1877  19.30  1881  nfeqf2  2382  nabbib  3045  r2exlem  3143  spc3gv  3604  vn0  4345  notzfaus  5363  dtruALT2  5370  dvdemo1  5373  dtruALT  5388  eunex  5390  reusv2lem2  5399  dtru  5441  dtruOLD  5446  brprcneu  6896  brprcneuALT  6897  dffv2  7004  zfcndpow  10656  hashfun  14476  nmo  32509  bnj1304  34833  bnj1253  35031  axrepprim  35702  axunprim  35703  axregprim  35705  axinfprim  35706  axacprim  35707  dftr6  35751  brtxpsd  35895  elfuns  35916  dfrdg4  35952  relowlpssretop  37365  onsupmaxb  43251  clsk3nimkb  44053  expandexn  44308  vk15.4j  44548  vk15.4jVD  44934  alneu  47136
  Copyright terms: Public domain W3C validator