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

Theorem exnal 1699
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 1698 . 2  |-  ( A. x ph  <->  -.  E. x  -.  ph )
21con2bii 334 1  |-  ( E. x  -.  ph  <->  -.  A. x ph )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    <-> wb 188   A.wal 1442   E.wex 1663
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682
This theorem depends on definitions:  df-bi 189  df-ex 1664
This theorem is referenced by:  alexn  1714  exanali  1721  19.35  1740  19.30  1744  excomOLD  1928  nfeqf2  2135  nabbi  2725  r2exlem  2910  spc3gv  3139  notzfaus  4578  dtru  4594  eunex  4596  reusv2lem2  4605  dtruALT  4632  dvdemo1  4635  dtruALT2  4644  brprcneu  5858  dffv2  5938  zfcndpow  9041  hashfun  12609  nmo  28121  bnj1304  29631  bnj1253  29826  axrepprim  30329  axunprim  30330  axregprim  30332  axinfprim  30333  axacprim  30334  dftr6  30390  brtxpsd  30661  elfuns  30682  dfrdg4  30718  bj-dtru  31412  bj-eunex  31414  bj-dvdemo1  31417  relowlpssretop  31767  vk15.4j  36885  vk15.4jVD  37311  alneu  38622
  Copyright terms: Public domain W3C validator