Theorem dmex 7911

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

Syntax hints:   ∈ wcel 2099  Vcvv 3469  dom cdm 5672

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698  ax-sep 5293  ax-nul 5300  ax-pr 5423  ax-un 7734

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-rab 3428  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-opab 5205  df-cnv 5680  df-dm 5682  df-rn 5683

This theorem is referenced by:  elxp4  7924  ofmres  7982  1stval  7989  fo1st  8007  frxp  8125  frxp2  8143  frxp3  8150  tfrlem8  8398  mapprc  8840  ixpprc  8929  bren  8965  brenOLD  8966  brdomg  8968  brdomgOLD  8969  fundmen  9047  domssex  9154  mapen  9157  ssenen  9167  hartogslem1  9557  wemapso  9566  brwdomn0  9584  unxpwdom2  9603  ixpiunwdom  9605  oemapwe  9709  cantnffval2  9710  r0weon  10027  fseqenlem2  10040  acndom  10066  acndom2  10069  dfac9  10151  ackbij2lem2  10255  ackbij2lem3  10256  cfsmolem  10285  coftr  10288  dcomex  10462  axdc3lem4  10468  axdclem  10534  axdclem2  10535  fodomb  10541  brdom3  10543  brdom5  10544  brdom4  10545  hashfacenOLD  14438  shftfval  15041  prdsvallem  17427  isoval  17739  issubc  17812  prfval  18181  psgnghm2  21500  psdmul  22077  dfac14  23509  indishmph  23689  ufldom  23853  tsmsval2  24021  dvmptadd  25879  dvmptmul  25880  dvmptco  25891  taylfval  26280  usgrsizedg  29015  usgredgleordALT  29034  vtxdun  29282  vtxdlfgrval  29286  vtxd0nedgb  29289  vtxdushgrfvedglem  29290  vtxdushgrfvedg  29291  vtxdginducedm1lem4  29343  vtxdginducedm1  29344  ewlksfval  29402  wksfval  29410  wksvOLD  29421  wlkiswwlksupgr2  29675  vdn0conngrumgrv2  29993  vdgn1frgrv2  30093  hmoval  30607  cyc3conja  32856  esum2d  33648  sitmval  33905  bnj893  34495  fmlafv  34926  fmla  34927  fmlasuc0  34930  dfrecs2  35482  dfrdg4  35483  indexdom  37142  dibfval  40551  aomclem1  42400  dfac21  42412  trclexi  42973  rtrclexi  42974  dfrtrcl5  42982  dfrcl2  43027  dvsubf  45225  dvdivf  45233  fouriersw  45542  smflimlem1  46082  smflimlem6  46087  smfpimcc  46119  smfsuplem1  46122  smfinflem  46128  smflimsuplem1  46131  smflimsuplem2  46132  smflimsuplem3  46133  smflimsuplem4  46134  smflimsuplem5  46135  smflimsuplem7  46137  smfliminflem  46141  fsupdm  46153  finfdm  46157  isuspgrim0  47093  grimidvtxedg  47097  upwlksfval  47120