Theorem dmex 7860

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

Step	Hyp	Ref	Expression
1		dmex.1	. 2 ⊢ 𝐴 ∈ V
2		dmexg 7852	. 2 ⊢ (𝐴 ∈ V → dom 𝐴 ∈ V)
3	1, 2	ax-mp 5	1 ⊢ dom 𝐴 ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3429  dom cdm 5631

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 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-cnv 5639  df-dm 5641  df-rn 5642

This theorem is referenced by:  elxp4  7873  ofmres  7937  1stval  7944  fo1st  7962  frxp  8076  frxp2  8094  frxp3  8101  tfrlem8  8323  mapprc  8777  ixpprc  8867  bren  8903  brdomg  8905  fundmen  8978  domssex  9076  mapen  9079  ssenen  9089  hartogslem1  9457  wemapso  9466  brwdomn0  9484  unxpwdom2  9503  ixpiunwdom  9505  oemapwe  9615  cantnffval2  9616  r0weon  9934  fseqenlem2  9947  acndom  9973  acndom2  9976  dfac9  10059  ackbij2lem2  10161  ackbij2lem3  10162  cfsmolem  10192  coftr  10195  dcomex  10369  axdc3lem4  10375  axdclem  10441  axdclem2  10442  fodomb  10448  brdom3  10450  brdom5  10451  brdom4  10452  shftfval  15032  prdsvallem  17417  isoval  17732  issubc  17802  prfval  18165  psgnghm2  21561  psdmul  22132  dfac14  23583  indishmph  23763  ufldom  23927  tsmsval2  24095  dvmptadd  25927  dvmptmul  25928  dvmptco  25939  taylfval  26324  usgrsizedg  29284  usgredgleordALT  29303  vtxdun  29550  vtxdlfgrval  29554  vtxd0nedgb  29557  vtxdushgrfvedglem  29558  vtxdushgrfvedg  29559  vtxdginducedm1lem4  29611  vtxdginducedm1  29612  ewlksfval  29670  wksfval  29678  wlkiswwlksupgr2  29945  vdn0conngrumgrv2  30266  vdgn1frgrv2  30366  hmoval  30881  cyc3conja  33218  esum2d  34237  sitmval  34493  bnj893  35070  fmlafv  35562  fmla  35563  fmlasuc0  35566  dfrecs2  36132  dfrdg4  36133  indexdom  38055  dibfval  41587  aomclem1  43482  dfac21  43494  trclexi  44047  rtrclexi  44048  dfrtrcl5  44056  dfrcl2  44101  dvsubf  46342  dvdivf  46350  fouriersw  46659  smflimlem1  47199  smflimlem6  47204  smfpimcc  47236  smfsuplem1  47239  smfinflem  47245  smflimsuplem1  47248  smflimsuplem2  47249  smflimsuplem3  47250  smflimsuplem4  47251  smflimsuplem5  47252  smflimsuplem7  47254  smfliminflem  47258  fsupdm  47270  finfdm  47274  grimidvtxedg  48361  isuspgrim0  48370  cycldlenngric  48404  upwlksfval  48611  dfinito4  49976  dftermo4  49977