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

Theorem dmex 4894
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 4892 . 2  |-  ( A  e.  _V  ->  dom  A  e.  _V )
31, 2ax-mp 10 1  |-  dom  A  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1621   _Vcvv 2740   dom cdm 4626
This theorem is referenced by:  elxp4  5112  ofmres  6015  1stval  6023  fo1st  6038  frxp  6124  tfrlem8  6333  mapprc  6709  ixpprc  6770  bren  6804  brdomg  6805  fundmen  6867  domssex  6955  mapen  6958  ssenen  6968  hartogslem1  7190  brwdomn0  7216  unxpwdom2  7235  ixpiunwdom  7238  oemapwe  7329  cantnffval2  7330  r0weon  7573  fseqenlem2  7585  acndom  7611  acndom2  7614  dfac9  7695  ackbij2lem2  7799  ackbij2lem3  7800  cfsmolem  7829  coftr  7832  dcomex  8006  axdc3lem4  8012  axdclem  8079  axdclem2  8080  fodomb  8084  brdom3  8086  brdom5  8087  brdom4  8088  hashfacen  11322  shftfval  11495  prdsval  13282  isoval  13594  issubc  13639  prfval  13900  symgbas  14699  dfac14  17239  indishmph  17416  ufldom  17584  tsmsval2  17739  dvmptadd  19236  dvmptmul  19237  dvmptco  19248  taylfval  19665  hmoval  21313  dfrdg4  23828  tfrqfree  23829  islatalg  24515  ishoma  25119  ishomb  25120  ismona  25141  isepia  25151  isiso  25157  cinvlem1  25160  cinvlem2  25161  isfunb  25167  infemb  25191  isinob  25194  propsrc  25200  indexdom  25745  aomclem1  26483  dfac21  26496  psgnghm2  26770  bnj893  27972  dibfval  30461
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-sep 4081  ax-nul 4089  ax-pr 4152  ax-un 4449
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2121  df-mo 2122  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-rex 2521  df-rab 2523  df-v 2742  df-dif 3097  df-un 3099  df-in 3101  df-ss 3108  df-nul 3398  df-if 3507  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3769  df-br 3964  df-opab 4018  df-cnv 4642  df-dm 4644  df-rn 4645
  Copyright terms: Public domain W3C validator