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

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

Proof of Theorem exnal
StepHypRef Expression
1 alex 1581 . 2  |-  ( A. x ph  <->  -.  E. x  -.  ph )
21con2bii 323 1  |-  ( E. x  -.  ph  <->  -.  A. x ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 177   A.wal 1549   E.wex 1550
This theorem is referenced by:  alexn  1589  exanali  1595  19.30  1614  excom  1756  equsexOLD  2003  ax12olem3  2007  ax12olem5OLD  2015  ax10lem2OLD  2026  spc3gv  3033  notzfaus  4366  dtru  4382  eunex  4384  dtruALT  4388  dvdemo1  4391  dtruALT2  4400  reusv2lem2  4716  brprcneu  5712  dffv2  5787  zfcndpow  8480  hashfun  11688  nmo  23961  axrepprim  25139  axunprim  25140  axregprim  25142  axinfprim  25143  axacprim  25144  dftr6  25362  brtxpsd  25689  dfrdg4  25745  alneu  27893  vk15.4j  28467  vk15.4jVD  28880  bnj1304  29045  bnj1253  29240  equsexNEW7  29344
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566
This theorem depends on definitions:  df-bi 178  df-ex 1551
  Copyright terms: Public domain W3C validator