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

Theorem exnal 1618
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 1617 . 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 1367   E.wex 1586
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602
This theorem depends on definitions:  df-bi 185  df-ex 1587
This theorem is referenced by:  alexn  1631  exanali  1637  19.35  1654  19.30  1659  excom  1787  nfeqf2  1989  nabbi  2701  spc3gv  3057  notzfaus  4462  dtru  4478  eunex  4480  reusv2lem2  4489  dtruALT  4519  dvdemo1  4522  dtruALT2  4531  brprcneu  5679  dffv2  5759  zfcndpow  8775  hashfun  12191  nmo  25837  axrepprim  27322  axunprim  27323  axregprim  27325  axinfprim  27326  axacprim  27327  dftr6  27529  brtxpsd  27894  elfuns  27915  dfrdg4  27950  alneu  29996  vk15.4j  31162  vk15.4jVD  31579  bnj1304  31742  bnj1253  31937  bj-dtru  32219  bj-eunex  32221  bj-dvdemo1  32224
  Copyright terms: Public domain W3C validator