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 2107  Vcvv 3475  dom cdm 5677

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-cnv 5685  df-dm 5687  df-rn 5688

This theorem is referenced by:  elxp4  7913  ofmres  7971  1stval  7977  fo1st  7995  frxp  8112  frxp2  8130  frxp3  8137  tfrlem8  8384  mapprc  8824  ixpprc  8913  bren  8949  brenOLD  8950  brdomg  8952  brdomgOLD  8953  fundmen  9031  domssex  9138  mapen  9141  ssenen  9151  hartogslem1  9537  wemapso  9546  brwdomn0  9564  unxpwdom2  9583  ixpiunwdom  9585  oemapwe  9689  cantnffval2  9690  r0weon  10007  fseqenlem2  10020  acndom  10046  acndom2  10049  dfac9  10131  ackbij2lem2  10235  ackbij2lem3  10236  cfsmolem  10265  coftr  10268  dcomex  10442  axdc3lem4  10448  axdclem  10514  axdclem2  10515  fodomb  10521  brdom3  10523  brdom5  10524  brdom4  10525  hashfacenOLD  14414  shftfval  15017  prdsvallem  17400  isoval  17712  issubc  17785  prfval  18151  psgnghm2  21134  dfac14  23122  indishmph  23302  ufldom  23466  tsmsval2  23634  dvmptadd  25477  dvmptmul  25478  dvmptco  25489  taylfval  25871  usgrsizedg  28472  usgredgleordALT  28491  vtxdun  28738  vtxdlfgrval  28742  vtxd0nedgb  28745  vtxdushgrfvedglem  28746  vtxdushgrfvedg  28747  vtxdginducedm1lem4  28799  vtxdginducedm1  28800  ewlksfval  28858  wksfval  28866  wksvOLD  28877  wlkiswwlksupgr2  29131  vdn0conngrumgrv2  29449  vdgn1frgrv2  29549  hmoval  30063  cyc3conja  32316  esum2d  33091  sitmval  33348  bnj893  33939  fmlafv  34371  fmla  34372  fmlasuc0  34375  dfrecs2  34922  dfrdg4  34923  indexdom  36602  dibfval  40012  aomclem1  41796  dfac21  41808  trclexi  42371  rtrclexi  42372  dfrtrcl5  42380  dfrcl2  42425  dvsubf  44630  dvdivf  44638  fouriersw  44947  smflimlem1  45487  smflimlem6  45492  smfpimcc  45524  smfsuplem1  45527  smfinflem  45533  smflimsuplem1  45536  smflimsuplem2  45537  smflimsuplem3  45538  smflimsuplem4  45539  smflimsuplem5  45540  smflimsuplem7  45542  smfliminflem  45546  fsupdm  45558  finfdm  45562  upwlksfval  46513