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

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

Proof of Theorem exnal
StepHypRef Expression
1 alex 1570 . 2  |-  ( A. x ph  <->  -.  E. x  -.  ph )
21con2bii 324 1  |-  ( E. x  -.  ph  <->  -.  A. x ph )
Colors of variables: wff set class
Syntax hints:   -. wn 5    <-> wb 178   A.wal 1532   E.wex 1537
This theorem is referenced by:  alexn  1577  exanali  1583  19.30  1603  ax12olem25  1659  ax10lem21  1670  equsex  1853  cla43gv  2841  notzfaus  4143  dtru  4159  eunex  4161  dtruALT  4165  dvdemo1  4168  dtruALT2  4177  reusv2lem2  4494  dffv2  5512  zfcndpow  8192  hashfun  11340  axrepprim  23406  axunprim  23407  axregprim  23409  axinfprim  23410  axacprim  23411  dftr6  23464  brtxpsd  23796  dfrdg4  23849  vk15.4j  27328  vk15.4jVD  27724  bnj1304  27885  bnj1253  28080  ax12olem25X  28231  ax10lem21X  28241  ax12-2  28254  ax12-3  28255  equsexv-x12  28264  a12study9  28271  a12peros  28272  a12study5rev  28273  a12studyALT  28284  ax9lem15  28305
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536
This theorem depends on definitions:  df-bi 179  df-ex 1538
  Copyright terms: Public domain W3C validator