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  27081  vk15.4jVD  27477  bnj1304  27638  bnj1253  27833  ax12olem25X  27984  ax10lem21X  27994  ax12-2  28007  ax12-3  28008  equsexv-x12  28017  a12study9  28024  a12peros  28025  a12study5rev  28026  a12studyALT  28037  ax9lem15  28058
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