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

Theorem exnal 1619
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 1618 . 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 1368   E.wex 1587
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603
This theorem depends on definitions:  df-bi 185  df-ex 1588
This theorem is referenced by:  alexn  1632  exanali  1638  19.35  1655  19.30  1660  excom  1789  nfeqf2  2001  nabbi  2784  nabbiOLD  2785  spc3gv  3166  notzfaus  4574  dtru  4590  eunex  4592  reusv2lem2  4601  dtruALT  4631  dvdemo1  4634  dtruALT2  4643  brprcneu  5791  dffv2  5872  zfcndpow  8893  hashfun  12316  nmo  26020  axrepprim  27496  axunprim  27497  axregprim  27499  axinfprim  27500  axacprim  27501  dftr6  27703  brtxpsd  28068  elfuns  28089  dfrdg4  28124  alneu  30172  vk15.4j  31550  vk15.4jVD  31967  bnj1304  32130  bnj1253  32325  bj-dtru  32635  bj-eunex  32637  bj-dvdemo1  32640
  Copyright terms: Public domain W3C validator