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

Theorem dmex 4943
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 4941 . 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 1686   _Vcvv 2790   dom cdm 4691
This theorem is referenced by:  elxp4  5162  ofmres  6118  1stval  6126  fo1st  6141  frxp  6227  tfrlem8  6402  mapprc  6778  ixpprc  6839  bren  6873  brdomg  6874  fundmen  6936  domssex  7024  mapen  7027  ssenen  7037  hartogslem1  7259  brwdomn0  7285  unxpwdom2  7304  ixpiunwdom  7307  oemapwe  7398  cantnffval2  7399  r0weon  7642  fseqenlem2  7654  acndom  7680  acndom2  7683  dfac9  7764  ackbij2lem2  7868  ackbij2lem3  7869  cfsmolem  7898  coftr  7901  dcomex  8075  axdc3lem4  8081  axdclem  8148  axdclem2  8149  fodomb  8153  brdom3  8155  brdom5  8156  brdom4  8157  hashfacen  11394  shftfval  11567  prdsval  13357  isoval  13669  issubc  13714  prfval  13975  symgbas  14774  dfac14  17314  indishmph  17491  ufldom  17659  tsmsval2  17814  dvmptadd  19311  dvmptmul  19312  dvmptco  19323  taylfval  19740  hmoval  21390  dfrdg4  24490  tfrqfree  24491  islatalg  25194  ishoma  25798  ishomb  25799  ismona  25820  isepia  25830  isiso  25836  cinvlem1  25839  cinvlem2  25840  isfunb  25846  infemb  25870  isinob  25873  propsrc  25879  indexdom  26424  aomclem1  27162  dfac21  27175  psgnghm2  27449  bnj893  29033  dibfval  31404
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pr 4216  ax-un 4514
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-rex 2551  df-rab 2554  df-v 2792  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-br 4026  df-opab 4080  df-cnv 4699  df-dm 4701  df-rn 4702
  Copyright terms: Public domain W3C validator