Theorem dmex 7949

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

Syntax hints:   ∈ wcel 2108  Vcvv 3488  dom cdm 5700

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-cnv 5708  df-dm 5710  df-rn 5711

This theorem is referenced by:  elxp4  7962  ofmres  8025  1stval  8032  fo1st  8050  frxp  8167  frxp2  8185  frxp3  8192  tfrlem8  8440  mapprc  8888  ixpprc  8977  bren  9013  brenOLD  9014  brdomg  9016  brdomgOLD  9017  fundmen  9096  domssex  9204  mapen  9207  ssenen  9217  hartogslem1  9611  wemapso  9620  brwdomn0  9638  unxpwdom2  9657  ixpiunwdom  9659  oemapwe  9763  cantnffval2  9764  r0weon  10081  fseqenlem2  10094  acndom  10120  acndom2  10123  dfac9  10206  ackbij2lem2  10308  ackbij2lem3  10309  cfsmolem  10339  coftr  10342  dcomex  10516  axdc3lem4  10522  axdclem  10588  axdclem2  10589  fodomb  10595  brdom3  10597  brdom5  10598  brdom4  10599  shftfval  15119  prdsvallem  17514  isoval  17826  issubc  17899  prfval  18268  psgnghm2  21622  psdmul  22193  dfac14  23647  indishmph  23827  ufldom  23991  tsmsval2  24159  dvmptadd  26018  dvmptmul  26019  dvmptco  26030  taylfval  26418  usgrsizedg  29250  usgredgleordALT  29269  vtxdun  29517  vtxdlfgrval  29521  vtxd0nedgb  29524  vtxdushgrfvedglem  29525  vtxdushgrfvedg  29526  vtxdginducedm1lem4  29578  vtxdginducedm1  29579  ewlksfval  29637  wksfval  29645  wksvOLD  29656  wlkiswwlksupgr2  29910  vdn0conngrumgrv2  30228  vdgn1frgrv2  30328  hmoval  30842  cyc3conja  33150  esum2d  34057  sitmval  34314  bnj893  34904  fmlafv  35348  fmla  35349  fmlasuc0  35352  dfrecs2  35914  dfrdg4  35915  indexdom  37694  dibfval  41098  aomclem1  43011  dfac21  43023  trclexi  43582  rtrclexi  43583  dfrtrcl5  43591  dfrcl2  43636  dvsubf  45835  dvdivf  45843  fouriersw  46152  smflimlem1  46692  smflimlem6  46697  smfpimcc  46729  smfsuplem1  46732  smfinflem  46738  smflimsuplem1  46741  smflimsuplem2  46742  smflimsuplem3  46743  smflimsuplem4  46744  smflimsuplem5  46745  smflimsuplem7  46747  smfliminflem  46751  fsupdm  46763  finfdm  46767  isuspgrim0  47756  grimidvtxedg  47760  upwlksfval  47858