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

Theorem exnal 1696
Description: Theorem 19.14 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
Assertion
Ref Expression
exnal  |-  ( E. x  -.  ph  <->  -.  A. x ph )

Proof of Theorem exnal
StepHypRef Expression
1 alex 1695 . 2  |-  ( A. x ph  <->  -.  E. x  -.  ph )
21con2bii 334 1  |-  ( E. x  -.  ph  <->  -.  A. x ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 188   A.wal 1436   E.wex 1660
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679
This theorem depends on definitions:  df-bi 189  df-ex 1661
This theorem is referenced by:  alexn  1710  exanali  1716  19.35  1733  19.30  1737  excomOLD  1901  nfeqf2  2097  nabbi  2759  nabbiOLD  2760  r2exlem  2949  spc3gv  3172  notzfaus  4597  dtru  4613  eunex  4615  reusv2lem2  4624  dtruALT  4651  dvdemo1  4654  dtruALT2  4663  brprcneu  5872  dffv2  5952  zfcndpow  9043  hashfun  12608  nmo  28113  bnj1304  29633  bnj1253  29828  axrepprim  30331  axunprim  30332  axregprim  30334  axinfprim  30335  axacprim  30336  dftr6  30391  brtxpsd  30660  elfuns  30681  dfrdg4  30717  bj-dtru  31376  bj-eunex  31378  bj-dvdemo1  31381  relowlpssretop  31725  vk15.4j  36787  vk15.4jVD  37216  alneu  38379
  Copyright terms: Public domain W3C validator