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

Theorem dmex 5099
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 5097 . 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 1721   _Vcvv 2924   dom cdm 4845
This theorem is referenced by:  elxp4  5324  ofmres  6310  1stval  6318  fo1st  6333  frxp  6423  tfrlem8  6612  mapprc  6989  ixpprc  7050  bren  7084  brdomg  7085  fundmen  7147  domssex  7235  mapen  7238  ssenen  7248  hartogslem1  7475  brwdomn0  7501  unxpwdom2  7520  ixpiunwdom  7523  oemapwe  7614  cantnffval2  7615  r0weon  7858  fseqenlem2  7870  acndom  7896  acndom2  7899  dfac9  7980  ackbij2lem2  8084  ackbij2lem3  8085  cfsmolem  8114  coftr  8117  dcomex  8291  axdc3lem4  8297  axdclem  8363  axdclem2  8364  fodomb  8368  brdom3  8370  brdom5  8371  brdom4  8372  hashfacen  11666  shftfval  11848  prdsval  13641  isoval  13953  issubc  13998  prfval  14259  symgbas  15058  dfac14  17611  indishmph  17791  ufldom  17955  tsmsval2  18120  dvmptadd  19807  dvmptmul  19808  dvmptco  19819  taylfval  20236  hmoval  22272  ctex  24061  sitmval  24622  dfrdg4  25711  tfrqfree  25712  indexdom  26334  aomclem1  27027  dfac21  27040  psgnghm2  27314  bnj893  29017  dibfval  31636
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-sep 4298  ax-nul 4306  ax-pr 4371  ax-un 4668
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-rex 2680  df-rab 2683  df-v 2926  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-nul 3597  df-if 3708  df-sn 3788  df-pr 3789  df-op 3791  df-uni 3984  df-br 4181  df-opab 4235  df-cnv 4853  df-dm 4855  df-rn 4856
  Copyright terms: Public domain W3C validator