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

Theorem dmex 6632
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 6630 . 2  |-  ( A  e.  _V  ->  dom  A  e.  _V )
31, 2ax-mp 5 1  |-  dom  A  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1826   _Vcvv 3034   dom cdm 4913
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pr 4601  ax-un 6491
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-rex 2738  df-rab 2741  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-br 4368  df-opab 4426  df-cnv 4921  df-dm 4923  df-rn 4924
This theorem is referenced by:  elxp4  6643  ofmres  6695  1stval  6701  fo1st  6719  frxp  6809  tfrlem8  6971  mapprc  7342  ixpprc  7409  bren  7444  brdomg  7445  fundmen  7508  domssex  7597  mapen  7600  ssenen  7610  hartogslem1  7882  brwdomn0  7910  unxpwdom2  7929  ixpiunwdom  7932  oemapwe  8026  cantnffval2  8027  oemapweOLD  8048  cantnffval2OLD  8049  r0weon  8303  fseqenlem2  8319  acndom  8345  acndom2  8348  dfac9  8429  ackbij2lem2  8533  ackbij2lem3  8534  cfsmolem  8563  coftr  8566  dcomex  8740  axdc3lem4  8746  axdclem  8812  axdclem2  8813  fodomb  8817  brdom3  8819  brdom5  8820  brdom4  8821  hashfacen  12407  shftfval  12905  prdsval  14862  isoval  15171  issubc  15241  prfval  15585  symgbas  16522  psgnghm2  18708  dfac14  20204  indishmph  20384  ufldom  20548  tsmsval2  20713  dvmptadd  22448  dvmptmul  22449  dvmptco  22460  taylfval  22839  hmoval  25842  ctex  27680  esum2d  28241  sitmval  28473  dfrdg4  29753  tfrqfree  29754  indexdom  30391  aomclem1  31166  dfac21  31178  dvsubf  31875  dvdivf  31885  fouriersw  32180  usgsizedg  32713  usgsizedgALT  32714  usgsizedgALT2  32715  bnj893  34333  dibfval  37281  dfrcl2  38211
  Copyright terms: Public domain W3C validator