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

Theorem exnal 1707
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 1706 . 2  |-  ( A. x ph  <->  -.  E. x  -.  ph )
21con2bii 339 1  |-  ( E. x  -.  ph  <->  -.  A. x ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 189   A.wal 1450   E.wex 1671
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690
This theorem depends on definitions:  df-bi 190  df-ex 1672
This theorem is referenced by:  alexn  1722  exanali  1729  19.35  1748  19.30  1752  excomOLD  1945  nfeqf2  2148  nabbi  2744  r2exlem  2899  spc3gv  3125  notzfaus  4576  dtru  4592  eunex  4594  reusv2lem2  4603  dtruALT  4632  dvdemo1  4635  dtruALT2  4644  brprcneu  5872  dffv2  5953  zfcndpow  9059  hashfun  12650  nmo  28200  bnj1304  29703  bnj1253  29898  axrepprim  30401  axunprim  30402  axregprim  30404  axinfprim  30405  axacprim  30406  dftr6  30461  brtxpsd  30732  elfuns  30753  dfrdg4  30789  bj-dtru  31478  bj-eunex  31480  bj-dvdemo1  31483  relowlpssretop  31837  vk15.4j  36955  vk15.4jVD  37374  alneu  38767
  Copyright terms: Public domain W3C validator