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

Theorem exnal 1572
 Description: Theorem 19.14 of [Margaris] p. 90. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
exnal

Proof of Theorem exnal
StepHypRef Expression
1 alex 1570 . 2
21con2bii 324 1
 Colors of variables: wff set class Syntax hints:   wn 5   wb 178  wal 1532  wex 1537 This theorem is referenced by:  alexn  1577  exanali  1583  19.30  1603  ax12olem25  1659  ax10lem21  1670  equsex  1852  cla43gv  2810  notzfaus  4079  dtru  4095  eunex  4097  dtruALT  4101  dvdemo1  4104  dtruALT2  4113  reusv2lem2  4427  dffv2  5444  zfcndpow  8118  hashfun  11266  axrepprim  23219  axunprim  23220  axregprim  23222  axinfprim  23223  axacprim  23224  dftr6  23277  brtxpsd  23609  dfrdg4  23662  vk15.4j  26984  vk15.4jVD  27380  bnj1304  27541  bnj1253  27736  ax12-2  27792  ax12-3  27793  equsexv-x12  27802  a12study9  27809  a12peros  27810  a12study5rev  27811  a12studyALT  27822  ax9lem15  27843 This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-gen 1536 This theorem depends on definitions:  df-bi 179  df-ex 1538
 Copyright terms: Public domain W3C validator