Theorem dmex 7902

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

Syntax hints:   ∈ wcel 2149  Vcvv 3463  dom cdm 5659

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5258  ax-pr 5402  ax-un 7730

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-cnv 5667  df-dm 5669  df-rn 5670

This theorem is referenced by:  elxp4  7915  ofmres  7977  1stval  7984  fo1st  8002  frxp  8118  frxp2  8136  frxp3  8143  tfrlem8  8367  mapprc  8824  ixpprc  8913  bren  8949  brdomg  8951  fundmen  9024  domssex  9122  mapen  9125  ssenen  9135  hartogslem1  9500  wemapso  9509  brwdomn0  9527  unxpwdom2  9546  ixpiunwdom  9548  oemapwe  9659  cantnffval2  9660  r0weon  9992  fseqenlem2  10005  acndom  10031  acndom2  10034  dfac9  10116  ackbij2lem2  10218  ackbij2lem3  10219  cfsmolem  10250  coftr  10253  dcomex  10427  axdc3lem4  10433  axdclem  10499  axdclem2  10500  fodomb  10506  brdom3  10508  brdom5  10509  brdom4  10510  shftfval  15103  prdsvallem  17503  isoval  17818  issubc  17888  prfval  18251  psgnghm2  21696  psdmul  22294  dfac14  23740  indishmph  23920  ufldom  24084  tsmsval2  24252  dvmptadd  26084  dvmptmul  26085  dvmptco  26096  taylfval  26484  usgrsizedg  29502  usgredgleordALT  29521  vtxdun  29768  vtxdlfgrval  29772  vtxd0nedgb  29775  vtxdushgrfvedglem  29776  vtxdushgrfvedg  29777  vtxdginducedm1lem4  29829  vtxdginducedm1  29830  ewlksfval  29888  wksfval  29896  wlkiswwlksupgr2  30163  vdn0conngrumgrv2  30484  vdgn1frgrv2  30584  hmoval  31099  cyc3conja  33414  esum2d  34424  sitmval  34680  bnj893  35257  fmlafv  35767  fmla  35768  fmlasuc0  35771  dfrecs2  36337  dfrdg4  36338  indexdom  38268  dibfval  41800  aomclem1  43666  dfac21  43678  trclexi  44231  rtrclexi  44232  dfrtrcl5  44240  dfrcl2  44285  dvsubf  46513  dvdivf  46521  fouriersw  46830  smflimlem1  47370  smflimlem6  47375  smfpimcc  47407  smfsuplem1  47410  smfinflem  47416  smflimsuplem1  47419  smflimsuplem2  47420  smflimsuplem3  47421  smflimsuplem4  47422  smflimsuplem5  47423  smflimsuplem7  47425  smfliminflem  47429  fsupdm  47441  finfdm  47445  grimidvtxedg  48532  isuspgrim0  48541  cycldlenngric  48575  upwlksfval  48782  dfinito4  50157  dftermo4  50158