Theorem dmex 7856

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

Syntax hints:   ∈ wcel 2119  Vcvv 3432  dom cdm 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4846  df-br 5080  df-opab 5142  df-cnv 5633  df-dm 5635  df-rn 5636

This theorem is referenced by:  elxp4  7869  ofmres  7933  1stval  7940  fo1st  7958  frxp  8073  frxp2  8091  frxp3  8098  tfrlem8  8320  mapprc  8774  ixpprc  8864  bren  8900  brdomg  8902  fundmen  8975  domssex  9073  mapen  9076  ssenen  9086  hartogslem1  9454  wemapso  9463  brwdomn0  9481  unxpwdom2  9500  ixpiunwdom  9502  oemapwe  9613  cantnffval2  9614  r0weon  9932  fseqenlem2  9945  acndom  9971  acndom2  9974  dfac9  10057  ackbij2lem2  10159  ackbij2lem3  10160  cfsmolem  10190  coftr  10193  dcomex  10367  axdc3lem4  10373  axdclem  10439  axdclem2  10440  fodomb  10446  brdom3  10448  brdom5  10449  brdom4  10450  shftfval  15030  prdsvallem  17415  isoval  17730  issubc  17800  prfval  18163  psgnghm2  21563  psdmul  22161  dfac14  23608  indishmph  23788  ufldom  23952  tsmsval2  24120  dvmptadd  25952  dvmptmul  25953  dvmptco  25964  taylfval  26349  usgrsizedg  29309  usgredgleordALT  29328  vtxdun  29575  vtxdlfgrval  29579  vtxd0nedgb  29582  vtxdushgrfvedglem  29583  vtxdushgrfvedg  29584  vtxdginducedm1lem4  29636  vtxdginducedm1  29637  ewlksfval  29695  wksfval  29703  wlkiswwlksupgr2  29970  vdn0conngrumgrv2  30291  vdgn1frgrv2  30391  hmoval  30906  cyc3conja  33245  esum2d  34284  sitmval  34540  bnj893  35117  fmlafv  35615  fmla  35616  fmlasuc0  35619  dfrecs2  36185  dfrdg4  36186  indexdom  38108  dibfval  41640  aomclem1  43506  dfac21  43518  trclexi  44071  rtrclexi  44072  dfrtrcl5  44080  dfrcl2  44125  dvsubf  46364  dvdivf  46372  fouriersw  46681  smflimlem1  47221  smflimlem6  47226  smfpimcc  47258  smfsuplem1  47261  smfinflem  47267  smflimsuplem1  47270  smflimsuplem2  47271  smflimsuplem3  47272  smflimsuplem4  47273  smflimsuplem5  47274  smflimsuplem7  47276  smfliminflem  47280  fsupdm  47292  finfdm  47296  grimidvtxedg  48383  isuspgrim0  48392  cycldlenngric  48426  upwlksfval  48633  dfinito4  49998  dftermo4  49999