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

Theorem dmex 7591
 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 𝐴 ∈ V
Assertion
Ref Expression
dmex dom 𝐴 ∈ V

Proof of Theorem dmex
StepHypRef Expression
1 dmex.1 . 2 𝐴 ∈ V
2 dmexg 7588 . 2 (𝐴 ∈ V → dom 𝐴 ∈ V)
31, 2ax-mp 5 1 dom 𝐴 ∈ V
 Colors of variables: wff setvar class Syntax hints:   ∈ wcel 2115  Vcvv 3471  dom cdm 5528 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793  ax-sep 5176  ax-nul 5183  ax-pr 5303  ax-un 7436 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2623  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-rab 3135  df-v 3473  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4267  df-if 4441  df-sn 4541  df-pr 4543  df-op 4547  df-uni 4812  df-br 5040  df-opab 5102  df-cnv 5536  df-dm 5538  df-rn 5539 This theorem is referenced by:  elxp4  7602  ofmres  7660  1stval  7666  fo1st  7684  frxp  7795  tfrlem8  7995  mapprc  8385  ixpprc  8458  bren  8493  brdomg  8494  fundmen  8558  domssex  8654  mapen  8657  ssenen  8667  hartogslem1  8982  brwdomn0  9009  unxpwdom2  9028  ixpiunwdom  9030  oemapwe  9133  cantnffval2  9134  r0weon  9415  fseqenlem2  9428  acndom  9454  acndom2  9457  dfac9  9539  ackbij2lem2  9639  ackbij2lem3  9640  cfsmolem  9669  coftr  9672  dcomex  9846  axdc3lem4  9852  axdclem  9918  axdclem2  9919  fodomb  9925  brdom3  9927  brdom5  9928  brdom4  9929  hashfacen  13796  shftfval  14408  prdsval  16706  isoval  17013  issubc  17083  prfval  17427  psgnghm2  20700  dfac14  22201  indishmph  22381  ufldom  22545  tsmsval2  22713  dvmptadd  24541  dvmptmul  24542  dvmptco  24553  taylfval  24932  usgrsizedg  26983  usgredgleordALT  27002  vtxdun  27249  vtxdlfgrval  27253  vtxd0nedgb  27256  vtxdushgrfvedglem  27257  vtxdushgrfvedg  27258  vtxdginducedm1lem4  27310  vtxdginducedm1  27311  ewlksfval  27369  wksfval  27377  wksv  27387  wlkiswwlksupgr2  27641  vdn0conngrumgrv2  27959  vdgn1frgrv2  28059  hmoval  28571  cyc3conja  30806  esum2d  31359  sitmval  31614  bnj893  32207  fmlafv  32634  fmla  32635  fmlasuc0  32638  dfrecs2  33418  dfrdg4  33419  indexdom  35050  dibfval  38315  aomclem1  39793  dfac21  39805  trclexi  40115  rtrclexi  40116  dfrtrcl5  40124  dfrcl2  40154  dvsubf  42347  dvdivf  42355  fouriersw  42664  smflimlem1  43195  smflimlem6  43200  smfpimcc  43230  smfsuplem1  43233  smfinflem  43239  smflimsuplem1  43242  smflimsuplem2  43243  smflimsuplem3  43244  smflimsuplem4  43245  smflimsuplem5  43246  smflimsuplem7  43248  smfliminflem  43252  upwlksfval  44155
 Copyright terms: Public domain W3C validator