Theorem dmex 7861

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

Syntax hints:   ∈ wcel 2114  Vcvv 3442  dom cdm 5632

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 2709  ax-sep 5243  ax-pr 5379  ax-un 7690

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 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-cnv 5640  df-dm 5642  df-rn 5643

This theorem is referenced by:  elxp4  7874  ofmres  7938  1stval  7945  fo1st  7963  frxp  8078  frxp2  8096  frxp3  8103  tfrlem8  8325  mapprc  8779  ixpprc  8869  bren  8905  brdomg  8907  fundmen  8980  domssex  9078  mapen  9081  ssenen  9091  hartogslem1  9459  wemapso  9468  brwdomn0  9486  unxpwdom2  9505  ixpiunwdom  9507  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  15005  prdsvallem  17386  isoval  17701  issubc  17771  prfval  18134  psgnghm2  21548  psdmul  22121  dfac14  23574  indishmph  23754  ufldom  23918  tsmsval2  24086  dvmptadd  25932  dvmptmul  25933  dvmptco  25944  taylfval  26334  usgrsizedg  29300  usgredgleordALT  29319  vtxdun  29567  vtxdlfgrval  29571  vtxd0nedgb  29574  vtxdushgrfvedglem  29575  vtxdushgrfvedg  29576  vtxdginducedm1lem4  29628  vtxdginducedm1  29629  ewlksfval  29687  wksfval  29695  wlkiswwlksupgr2  29962  vdn0conngrumgrv2  30283  vdgn1frgrv2  30383  hmoval  30897  cyc3conja  33250  esum2d  34270  sitmval  34526  bnj893  35103  fmlafv  35593  fmla  35594  fmlasuc0  35597  dfrecs2  36163  dfrdg4  36164  indexdom  37982  dibfval  41514  aomclem1  43408  dfac21  43420  trclexi  43973  rtrclexi  43974  dfrtrcl5  43982  dfrcl2  44027  dvsubf  46269  dvdivf  46277  fouriersw  46586  smflimlem1  47126  smflimlem6  47131  smfpimcc  47163  smfsuplem1  47166  smfinflem  47172  smflimsuplem1  47175  smflimsuplem2  47176  smflimsuplem3  47177  smflimsuplem4  47178  smflimsuplem5  47179  smflimsuplem7  47181  smfliminflem  47185  fsupdm  47197  finfdm  47201  grimidvtxedg  48242  isuspgrim0  48251  cycldlenngric  48285  upwlksfval  48492  dfinito4  49857  dftermo4  49858