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

Theorem exnal 1752
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 1751 . 2 (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
21con2bii 347 1 (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wal 1479  wex 1702
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735
This theorem depends on definitions:  df-bi 197  df-ex 1703
This theorem is referenced by:  alexn  1769  exanali  1784  19.35  1803  19.30  1807  nfeqf2  2295  nabbi  2893  r2exlem  3055  spc3gv  3293  notzfaus  4831  dtru  4848  eunex  4850  reusv2lem2  4860  reusv2lem2OLD  4861  dtruALT  4890  dvdemo1  4893  dtruALT2  4902  brprcneu  6171  dffv2  6258  zfcndpow  9423  hashfun  13207  nmo  29297  bnj1304  30864  bnj1253  31059  axrepprim  31553  axunprim  31554  axregprim  31556  axinfprim  31557  axacprim  31558  dftr6  31615  brtxpsd  31976  elfuns  31997  dfrdg4  32033  bj-dtru  32772  bj-eunex  32774  bj-dvdemo1  32777  relowlpssretop  33183  wl-dveeq12  33282  clsk3nimkb  38158  vk15.4j  38554  vk15.4jVD  38970  alneu  40964
  Copyright terms: Public domain W3C validator