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

Theorem exnal 1561
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 1559 . 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 1527   E.wex 1528
This theorem is referenced by:  alexn  1566  exanali  1572  19.30  1591  ax12olem5  1872  ax10lem2  1877  equsex  1902  spc3gv  2873  notzfaus  4185  dtru  4201  eunex  4203  dtruALT  4207  dvdemo1  4210  dtruALT2  4219  reusv2lem2  4536  brprcneu  5518  dffv2  5592  zfcndpow  8238  hashfun  11389  nmo  23144  axrepprim  24048  axunprim  24049  axregprim  24051  axinfprim  24052  axacprim  24053  dftr6  24107  brtxpsd  24434  dfrdg4  24488  vk15.4j  28291  vk15.4jVD  28690  bnj1304  28852  bnj1253  29047  ax12-2  29103  ax12-3  29104  equsexv-x12  29113  a12study9  29120  a12peros  29121  a12study5rev  29122  a12studyALT  29133  ax9lem15  29154
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544
This theorem depends on definitions:  df-bi 177  df-ex 1529
  Copyright terms: Public domain W3C validator