Theorem dmex 7865

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

Syntax hints:   ∈ wcel 2109  Vcvv 3444  dom cdm 5631

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 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382  ax-un 7691

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 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-cnv 5639  df-dm 5641  df-rn 5642

This theorem is referenced by:  elxp4  7878  ofmres  7942  1stval  7949  fo1st  7967  frxp  8082  frxp2  8100  frxp3  8107  tfrlem8  8329  mapprc  8780  ixpprc  8869  bren  8905  brdomg  8907  fundmen  8979  domssex  9079  mapen  9082  ssenen  9092  hartogslem1  9471  wemapso  9480  brwdomn0  9498  unxpwdom2  9517  ixpiunwdom  9519  oemapwe  9623  cantnffval2  9624  r0weon  9941  fseqenlem2  9954  acndom  9980  acndom2  9983  dfac9  10066  ackbij2lem2  10168  ackbij2lem3  10169  cfsmolem  10199  coftr  10202  dcomex  10376  axdc3lem4  10382  axdclem  10448  axdclem2  10449  fodomb  10455  brdom3  10457  brdom5  10458  brdom4  10459  shftfval  15012  prdsvallem  17393  isoval  17703  issubc  17773  prfval  18136  psgnghm2  21466  psdmul  22029  dfac14  23481  indishmph  23661  ufldom  23825  tsmsval2  23993  dvmptadd  25840  dvmptmul  25841  dvmptco  25852  taylfval  26242  usgrsizedg  29118  usgredgleordALT  29137  vtxdun  29385  vtxdlfgrval  29389  vtxd0nedgb  29392  vtxdushgrfvedglem  29393  vtxdushgrfvedg  29394  vtxdginducedm1lem4  29446  vtxdginducedm1  29447  ewlksfval  29505  wksfval  29513  wlkiswwlksupgr2  29780  vdn0conngrumgrv2  30098  vdgn1frgrv2  30198  hmoval  30712  cyc3conja  33087  esum2d  34056  sitmval  34313  bnj893  34891  fmlafv  35340  fmla  35341  fmlasuc0  35344  dfrecs2  35911  dfrdg4  35912  indexdom  37701  dibfval  41108  aomclem1  43016  dfac21  43028  trclexi  43582  rtrclexi  43583  dfrtrcl5  43591  dfrcl2  43636  dvsubf  45885  dvdivf  45893  fouriersw  46202  smflimlem1  46742  smflimlem6  46747  smfpimcc  46779  smfsuplem1  46782  smfinflem  46788  smflimsuplem1  46791  smflimsuplem2  46792  smflimsuplem3  46793  smflimsuplem4  46794  smflimsuplem5  46795  smflimsuplem7  46797  smfliminflem  46801  fsupdm  46813  finfdm  46817  grimidvtxedg  47858  isuspgrim0  47867  cycldlenngric  47901  upwlksfval  48096  dfinito4  49463  dftermo4  49464