Theorem dmex 7931

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

Syntax hints:   ∈ wcel 2105  Vcvv 3477  dom cdm 5688

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-cnv 5696  df-dm 5698  df-rn 5699

This theorem is referenced by:  elxp4  7944  ofmres  8007  1stval  8014  fo1st  8032  frxp  8149  frxp2  8167  frxp3  8174  tfrlem8  8422  mapprc  8868  ixpprc  8957  bren  8993  brdomg  8995  brdomgOLD  8996  fundmen  9069  domssex  9176  mapen  9179  ssenen  9189  hartogslem1  9579  wemapso  9588  brwdomn0  9606  unxpwdom2  9625  ixpiunwdom  9627  oemapwe  9731  cantnffval2  9732  r0weon  10049  fseqenlem2  10062  acndom  10088  acndom2  10091  dfac9  10174  ackbij2lem2  10276  ackbij2lem3  10277  cfsmolem  10307  coftr  10310  dcomex  10484  axdc3lem4  10490  axdclem  10556  axdclem2  10557  fodomb  10563  brdom3  10565  brdom5  10566  brdom4  10567  shftfval  15105  prdsvallem  17500  isoval  17812  issubc  17885  prfval  18254  psgnghm2  21616  psdmul  22187  dfac14  23641  indishmph  23821  ufldom  23985  tsmsval2  24153  dvmptadd  26012  dvmptmul  26013  dvmptco  26024  taylfval  26414  usgrsizedg  29246  usgredgleordALT  29265  vtxdun  29513  vtxdlfgrval  29517  vtxd0nedgb  29520  vtxdushgrfvedglem  29521  vtxdushgrfvedg  29522  vtxdginducedm1lem4  29574  vtxdginducedm1  29575  ewlksfval  29633  wksfval  29641  wksvOLD  29652  wlkiswwlksupgr2  29906  vdn0conngrumgrv2  30224  vdgn1frgrv2  30324  hmoval  30838  cyc3conja  33159  esum2d  34073  sitmval  34330  bnj893  34920  fmlafv  35364  fmla  35365  fmlasuc0  35368  dfrecs2  35931  dfrdg4  35932  indexdom  37720  dibfval  41123  aomclem1  43042  dfac21  43054  trclexi  43609  rtrclexi  43610  dfrtrcl5  43618  dfrcl2  43663  dvsubf  45869  dvdivf  45877  fouriersw  46186  smflimlem1  46726  smflimlem6  46731  smfpimcc  46763  smfsuplem1  46766  smfinflem  46772  smflimsuplem1  46775  smflimsuplem2  46776  smflimsuplem3  46777  smflimsuplem4  46778  smflimsuplem5  46779  smflimsuplem7  46781  smfliminflem  46785  fsupdm  46797  finfdm  46801  isuspgrim0  47809  grimidvtxedg  47813  upwlksfval  47978