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

Theorem exnal 1580
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 1578 . 2  |-  ( A. x ph  <->  -.  E. x  -.  ph )
21con2bii 323 1  |-  ( E. x  -.  ph  <->  -.  A. x ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 177   A.wal 1546   E.wex 1547
This theorem is referenced by:  alexn  1586  exanali  1592  19.30  1611  excom  1752  equsexOLD  1970  ax12olem3  1974  ax12olem5OLD  1981  ax10lem2OLD  1992  spc3gv  3001  notzfaus  4334  dtru  4350  eunex  4352  dtruALT  4356  dvdemo1  4359  dtruALT2  4368  reusv2lem2  4684  brprcneu  5680  dffv2  5755  zfcndpow  8447  hashfun  11655  nmo  23926  axrepprim  25104  axunprim  25105  axregprim  25107  axinfprim  25108  axacprim  25109  dftr6  25321  brtxpsd  25648  dfrdg4  25703  alneu  27846  vk15.4j  28323  vk15.4jVD  28735  bnj1304  28897  bnj1253  29092  equsexNEW7  29196
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563
This theorem depends on definitions:  df-bi 178  df-ex 1548
  Copyright terms: Public domain W3C validator