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

Theorem dmex 4848
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 4846 . 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 2727   dom cdm 4580
This theorem is referenced by:  elxp4  5066  ofmres  5968  1stval  5976  fo1st  5991  frxp  6077  tfrlem8  6286  mapprc  6662  ixpprc  6723  bren  6757  brdomg  6758  fundmen  6819  domssex  6907  mapen  6910  ssenen  6920  hartogslem1  7141  brwdomn0  7167  unxpwdom2  7186  ixpiunwdom  7189  oemapwe  7280  cantnffval2  7281  r0weon  7524  fseqenlem2  7536  acndom  7562  acndom2  7565  dfac9  7646  ackbij2lem2  7750  ackbij2lem3  7751  cfsmolem  7780  coftr  7783  dcomex  7957  axdc3lem4  7963  axdclem  8030  axdclem2  8031  fodomb  8035  brdom3  8037  brdom5  8038  brdom4  8039  hashfacen  11269  shftfval  11442  prdsval  13229  isoval  13511  issubc  13556  prfval  13817  symgbas  14607  dfac14  17144  indishmph  17321  ufldom  17489  tsmsval2  17644  dvmptadd  19141  dvmptmul  19142  dvmptco  19153  taylfval  19570  hmoval  21218  dfrdg4  23662  tfrqfree  23663  islatalg  24349  ishoma  24953  ishomb  24954  ismona  24975  isepia  24985  isiso  24991  cinvlem1  24994  cinvlem2  24995  isfunb  25001  infemb  25025  isinob  25028  propsrc  25034  indexdom  25579  aomclem1  26317  dfac21  26330  psgnghm2  26604  bnj893  27649  dibfval  30132
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 1926  ax-ext 2234  ax-sep 4038  ax-nul 4046  ax-pr 4108  ax-un 4403
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 1883  df-eu 2118  df-mo 2119  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-rex 2514  df-rab 2516  df-v 2729  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-nul 3363  df-if 3471  df-sn 3550  df-pr 3551  df-op 3553  df-uni 3728  df-br 3921  df-opab 3975  df-cnv 4596  df-dm 4598  df-rn 4599
  Copyright terms: Public domain W3C validator