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  1852  cla43gv  2810  notzfaus  4079  dtru  4095  eunex  4097  dtruALT  4101  dvdemo1  4104  dtruALT2  4113  reusv2lem2  4427  dffv2  5444  zfcndpow  8118  hashfun  11266  axrepprim  23219  axunprim  23220  axregprim  23222  axinfprim  23223  axacprim  23224  dftr6  23277  brtxpsd  23609  dfrdg4  23662  vk15.4j  26984  vk15.4jVD  27380  bnj1304  27541  bnj1253  27736  ax12-2  27792  ax12-3  27793  equsexv-x12  27802  a12study9  27809  a12peros  27810  a12study5rev  27811  a12studyALT  27822  ax9lem15  27843
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