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

Theorem exnal 1648
Description: Theorem 19.14 of [Margaris] p. 90. (Contributed by NM, 12-Mar-1993.)
Assertion
Ref Expression
exnal

Proof of Theorem exnal
StepHypRef Expression
1 alex 1647 . 2
21con2bii 332 1
Colors of variables: wff setvar class
Syntax hints:  -.wn 3  <->wb 184  A.wal 1393  E.wex 1612
This theorem is referenced by:  alexn  1664  exanali  1670  19.35  1687  19.30  1692  excom  1849  nfeqf2  2041  nabbi  2790  nabbiOLD  2791  r2exlem  2977  spc3gv  3199  notzfaus  4627  dtru  4643  eunex  4645  reusv2lem2  4654  dtruALT  4684  dvdemo1  4687  dtruALT2  4696  brprcneu  5864  dffv2  5946  zfcndpow  9015  hashfun  12495  nmo  27384  axrepprim  29074  axunprim  29075  axregprim  29077  axinfprim  29078  axacprim  29079  dftr6  29179  brtxpsd  29544  elfuns  29565  dfrdg4  29600  alneu  32206  vk15.4j  33298  vk15.4jVD  33714  bnj1304  33878  bnj1253  34073  bj-dtru  34383  bj-eunex  34385  bj-dvdemo1  34388
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631
This theorem depends on definitions:  df-bi 185  df-ex 1613
  Copyright terms: Public domain W3C validator