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

Theorem exnal 1744
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 1743 . 2 (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
21con2bii 346 1 (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 195  wal 1473  wex 1695
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728
This theorem depends on definitions:  df-bi 196  df-ex 1696
This theorem is referenced by:  alexn  1760  exanali  1773  19.35  1794  19.30  1798  nfeqf2  2285  nabbi  2884  r2exlem  3041  spc3gv  3271  notzfaus  4766  dtru  4783  eunex  4785  reusv2lem2  4795  reusv2lem2OLD  4796  dtruALT  4826  dvdemo1  4829  dtruALT2  4838  brprcneu  6096  dffv2  6181  zfcndpow  9317  hashfun  13084  nmo  28709  bnj1304  30144  bnj1253  30339  axrepprim  30833  axunprim  30834  axregprim  30836  axinfprim  30837  axacprim  30838  dftr6  30893  brtxpsd  31171  elfuns  31192  dfrdg4  31228  bj-dtru  31985  bj-eunex  31987  bj-dvdemo1  31990  relowlpssretop  32388  wl-dveeq12  32490  clsk3nimkb  37358  vk15.4j  37755  vk15.4jVD  38172  alneu  39850
  Copyright terms: Public domain W3C validator