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

Theorem exnal 1628
Description: Theorem 19.14 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
Assertion
Ref Expression
exnal  |-  ( E. x  -.  ph  <->  -.  A. x ph )

Proof of Theorem exnal
StepHypRef Expression
1 alex 1627 . 2  |-  ( A. x ph  <->  -.  E. x  -.  ph )
21con2bii 332 1  |-  ( E. x  -.  ph  <->  -.  A. x ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184   A.wal 1377   E.wex 1596
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612
This theorem depends on definitions:  df-bi 185  df-ex 1597
This theorem is referenced by:  alexn  1641  exanali  1647  19.35  1664  19.30  1669  excom  1798  nfeqf2  2014  nabbi  2800  nabbiOLD  2801  r2exlem  2982  spc3gv  3203  notzfaus  4622  dtru  4638  eunex  4640  reusv2lem2  4649  dtruALT  4679  dvdemo1  4682  dtruALT2  4691  brprcneu  5857  dffv2  5938  zfcndpow  8990  hashfun  12457  nmo  27060  axrepprim  28549  axunprim  28550  axregprim  28552  axinfprim  28553  axacprim  28554  dftr6  28756  brtxpsd  29121  elfuns  29142  dfrdg4  29177  alneu  31673  vk15.4j  32377  vk15.4jVD  32794  bnj1304  32957  bnj1253  33152  bj-dtru  33464  bj-eunex  33466  bj-dvdemo1  33469
  Copyright terms: Public domain W3C validator