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

Theorem exnal 1902
 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 1901 . 2 (∀𝑥𝜑 ↔ ¬ ∃𝑥 ¬ 𝜑)
21con2bii 346 1 (∃𝑥 ¬ 𝜑 ↔ ¬ ∀𝑥𝜑)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 196  ∀wal 1629  ∃wex 1852 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885 This theorem depends on definitions:  df-bi 197  df-ex 1853 This theorem is referenced by:  alexn  1921  exanali  1937  19.35  1957  19.30  1961  nfeqf2  2452  nfeqf2OLD  2453  nabbi  3045  r2exlem  3207  spc3gv  3449  notzfaus  4971  dtru  4988  eunex  4990  reusv2lem2  4999  dtruALT  5027  dvdemo1  5030  dtruALT2  5039  brprcneu  6325  dffv2  6413  zfcndpow  9640  hashfun  13426  nmo  29665  bnj1304  31228  bnj1253  31423  axrepprim  31917  axunprim  31918  axregprim  31920  axinfprim  31921  axacprim  31922  dftr6  31978  brtxpsd  32338  elfuns  32359  dfrdg4  32395  bj-dtru  33133  bj-eunex  33135  bj-dvdemo1  33138  relowlpssretop  33549  clsk3nimkb  38864  vk15.4j  39259  vk15.4jVD  39672  alneu  41721
 Copyright terms: Public domain W3C validator