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

Theorem exnal 1562
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 1560 . 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 1528   E.wex 1529
This theorem is referenced by:  alexn  1567  exanali  1573  19.30  1592  ax12olem5  1873  ax10lem2  1878  equsex  1904  spc3gv  2874  notzfaus  4184  dtru  4200  eunex  4202  dtruALT  4206  dvdemo1  4209  dtruALT2  4218  reusv2lem2  4535  dffv2  5553  zfcndpow  8233  hashfun  11383  axrepprim  23452  axunprim  23453  axregprim  23455  axinfprim  23456  axacprim  23457  dftr6  23510  brtxpsd  23842  dfrdg4  23895  vk15.4j  27562  vk15.4jVD  27958  bnj1304  28119  bnj1253  28314  ax12-2  28370  ax12-3  28371  equsexv-x12  28380  a12study9  28387  a12peros  28388  a12study5rev  28389  a12studyALT  28400  ax9lem15  28421
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545
This theorem depends on definitions:  df-bi 179  df-ex 1530
  Copyright terms: Public domain W3C validator