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

Theorem exnal 1903
Description: 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 1902 . 2 (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
21con2bii 346 1 (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wal 1630  wex 1853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886
This theorem depends on definitions:  df-bi 197  df-ex 1854
This theorem is referenced by:  alexn  1920  exanali  1935  19.35  1954  19.30  1958  nfeqf2  2442  nabbi  3034  r2exlem  3197  spc3gv  3438  notzfaus  4989  dtru  5006  eunex  5008  reusv2lem2  5018  reusv2lem2OLD  5019  dtruALT  5048  dvdemo1  5051  dtruALT2  5060  brprcneu  6345  dffv2  6433  zfcndpow  9630  hashfun  13416  nmo  29634  bnj1304  31197  bnj1253  31392  axrepprim  31886  axunprim  31887  axregprim  31889  axinfprim  31890  axacprim  31891  dftr6  31947  brtxpsd  32307  elfuns  32328  dfrdg4  32364  bj-dtru  33103  bj-eunex  33105  bj-dvdemo1  33108  relowlpssretop  33523  wl-dveeq12  33624  clsk3nimkb  38840  vk15.4j  39236  vk15.4jVD  39649  alneu  41707
  Copyright terms: Public domain W3C validator