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

Theorem dmex 4941
Description: The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring] p. 26. (Contributed by NM, 7-Jul-2008.)
Hypothesis
Ref Expression
dmex.1  |-  A  e. 
_V
Assertion
Ref Expression
dmex  |-  dom  A  e.  _V

Proof of Theorem dmex
StepHypRef Expression
1 dmex.1 . 2  |-  A  e. 
_V
2 dmexg 4939 . 2  |-  ( A  e.  _V  ->  dom  A  e.  _V )
31, 2ax-mp 8 1  |-  dom  A  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1684   _Vcvv 2788   dom cdm 4689
This theorem is referenced by:  elxp4  5160  ofmres  6116  1stval  6124  fo1st  6139  frxp  6225  tfrlem8  6400  mapprc  6776  ixpprc  6837  bren  6871  brdomg  6872  fundmen  6934  domssex  7022  mapen  7025  ssenen  7035  hartogslem1  7257  brwdomn0  7283  unxpwdom2  7302  ixpiunwdom  7305  oemapwe  7396  cantnffval2  7397  r0weon  7640  fseqenlem2  7652  acndom  7678  acndom2  7681  dfac9  7762  ackbij2lem2  7866  ackbij2lem3  7867  cfsmolem  7896  coftr  7899  dcomex  8073  axdc3lem4  8079  axdclem  8146  axdclem2  8147  fodomb  8151  brdom3  8153  brdom5  8154  brdom4  8155  hashfacen  11392  shftfval  11565  prdsval  13355  isoval  13667  issubc  13712  prfval  13973  symgbas  14772  dfac14  17312  indishmph  17489  ufldom  17657  tsmsval2  17812  dvmptadd  19309  dvmptmul  19310  dvmptco  19321  taylfval  19738  hmoval  21388  dfrdg4  24488  tfrqfree  24489  islatalg  25183  ishoma  25787  ishomb  25788  ismona  25809  isepia  25819  isiso  25825  cinvlem1  25828  cinvlem2  25829  isfunb  25835  infemb  25859  isinob  25862  propsrc  25868  indexdom  26413  aomclem1  27151  dfac21  27164  psgnghm2  27438  bnj893  28960  dibfval  31331
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214  ax-un 4512
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-cnv 4697  df-dm 4699  df-rn 4700
  Copyright terms: Public domain W3C validator