Theorem dmex 7910

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 7902	. 2 ⊢ (𝐴 ∈ V → dom 𝐴 ∈ V)
3	1, 2	ax-mp 5	1 ⊢ dom 𝐴 ∈ V

Syntax hints:   ∈ wcel 2109  Vcvv 3464  dom cdm 5659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407  ax-un 7734

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-cnv 5667  df-dm 5669  df-rn 5670

This theorem is referenced by:  elxp4  7923  ofmres  7988  1stval  7995  fo1st  8013  frxp  8130  frxp2  8148  frxp3  8155  tfrlem8  8403  mapprc  8849  ixpprc  8938  bren  8974  brdomg  8976  brdomgOLD  8977  fundmen  9050  domssex  9157  mapen  9160  ssenen  9170  hartogslem1  9561  wemapso  9570  brwdomn0  9588  unxpwdom2  9607  ixpiunwdom  9609  oemapwe  9713  cantnffval2  9714  r0weon  10031  fseqenlem2  10044  acndom  10070  acndom2  10073  dfac9  10156  ackbij2lem2  10258  ackbij2lem3  10259  cfsmolem  10289  coftr  10292  dcomex  10466  axdc3lem4  10472  axdclem  10538  axdclem2  10539  fodomb  10545  brdom3  10547  brdom5  10548  brdom4  10549  shftfval  15094  prdsvallem  17473  isoval  17783  issubc  17853  prfval  18216  psgnghm2  21546  psdmul  22109  dfac14  23561  indishmph  23741  ufldom  23905  tsmsval2  24073  dvmptadd  25921  dvmptmul  25922  dvmptco  25933  taylfval  26323  usgrsizedg  29199  usgredgleordALT  29218  vtxdun  29466  vtxdlfgrval  29470  vtxd0nedgb  29473  vtxdushgrfvedglem  29474  vtxdushgrfvedg  29475  vtxdginducedm1lem4  29527  vtxdginducedm1  29528  ewlksfval  29586  wksfval  29594  wksvOLD  29605  wlkiswwlksupgr2  29864  vdn0conngrumgrv2  30182  vdgn1frgrv2  30282  hmoval  30796  cyc3conja  33173  esum2d  34129  sitmval  34386  bnj893  34964  fmlafv  35407  fmla  35408  fmlasuc0  35411  dfrecs2  35973  dfrdg4  35974  indexdom  37763  dibfval  41165  aomclem1  43053  dfac21  43065  trclexi  43619  rtrclexi  43620  dfrtrcl5  43628  dfrcl2  43673  dvsubf  45923  dvdivf  45931  fouriersw  46240  smflimlem1  46780  smflimlem6  46785  smfpimcc  46817  smfsuplem1  46820  smfinflem  46826  smflimsuplem1  46829  smflimsuplem2  46830  smflimsuplem3  46831  smflimsuplem4  46832  smflimsuplem5  46833  smflimsuplem7  46835  smfliminflem  46839  fsupdm  46851  finfdm  46855  grimidvtxedg  47878  isuspgrim0  47887  cycldlenngric  47921  upwlksfval  48090  dfinito4  49366  dftermo4  49367