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

Theorem exnal 1669
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 1668 . 2  |-  ( A. x ph  <->  -.  E. x  -.  ph )
21con2bii 330 1  |-  ( E. x  -.  ph  <->  -.  A. x ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 184   A.wal 1403   E.wex 1633
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652
This theorem depends on definitions:  df-bi 185  df-ex 1634
This theorem is referenced by:  alexn  1685  exanali  1691  19.35  1708  19.30  1713  excom  1873  nfeqf2  2067  nabbi  2737  nabbiOLD  2738  r2exlem  2927  spc3gv  3149  notzfaus  4569  dtru  4585  eunex  4587  reusv2lem2  4596  dtruALT  4623  dvdemo1  4626  dtruALT2  4635  brprcneu  5842  dffv2  5922  zfcndpow  9024  hashfun  12544  nmo  27799  bnj1304  29205  bnj1253  29400  axrepprim  29903  axunprim  29904  axregprim  29906  axinfprim  29907  axacprim  29908  dftr6  29963  brtxpsd  30232  elfuns  30253  dfrdg4  30289  bj-dtru  30947  bj-eunex  30949  bj-dvdemo1  30952  relowlpssretop  31281  vk15.4j  36315  vk15.4jVD  36745  alneu  37574
  Copyright terms: Public domain W3C validator