NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  exnal Unicode version

Theorem exnal 1574
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 1572 . 2
21con2bii 322 1
Colors of variables: wff setvar class
Syntax hints:   wn 3   wb 176  wal 1540  wex 1541
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557
This theorem depends on definitions:  df-bi 177  df-ex 1542
This theorem is referenced by:  alexn  1579  exanali  1585  19.30  1604  excom  1741  ax12olem5  1931  ax10lem2  1937  equsex  1962  spc3gv  2944  necompl  3544  opkelimagekg  4271  dfpw2  4327  dfaddc2  4381  nnsucelrlem1  4424  eqpw1relk  4479  eqtfinrelk  4486  setconslem2  4732  setconslem3  4733  setconslem7  4737  dfswap2  4741  nfunv  5138  brimage  5793  releqel  5807  releqmpt2  5809  ovcelem1  6171  tcfnex  6244  nchoicelem10  6298  fnfreclem1  6317
  Copyright terms: Public domain W3C validator