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

Theorem exnal 1564
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 1562 . 2  |-  ( A. x ph  <->  -.  E. x  -.  ph )
21con2bii 322 1  |-  ( E. x  -.  ph  <->  -.  A. x ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 176   A.wal 1530   E.wex 1531
This theorem is referenced by:  alexn  1569  exanali  1575  19.30  1594  ax12olem5  1884  ax10lem2  1890  equsex  1915  spc3gv  2886  notzfaus  4201  dtru  4217  eunex  4219  dtruALT  4223  dvdemo1  4226  dtruALT2  4235  reusv2lem2  4552  brprcneu  5534  dffv2  5608  zfcndpow  8254  hashfun  11405  nmo  23160  axrepprim  24063  axunprim  24064  axregprim  24066  axinfprim  24067  axacprim  24068  dftr6  24178  brtxpsd  24505  dfrdg4  24560  alneu  28082  vk15.4j  28590  vk15.4jVD  29006  bnj1304  29168  bnj1253  29363  equsexNEW7  29467  ax12-2  29725  ax12-3  29726  equsexv-x12  29735  a12study9  29742  a12peros  29743  a12study5rev  29744  a12studyALT  29755  ax9lem15  29776
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547
This theorem depends on definitions:  df-bi 177  df-ex 1532
  Copyright terms: Public domain W3C validator