Theorem dmex 7834

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

Syntax hints:   ∈ wcel 2111  Vcvv 3436  dom cdm 5611

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365  ax-un 7663

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-opab 5149  df-cnv 5619  df-dm 5621  df-rn 5622

This theorem is referenced by:  elxp4  7847  ofmres  7911  1stval  7918  fo1st  7936  frxp  8051  frxp2  8069  frxp3  8076  tfrlem8  8298  mapprc  8749  ixpprc  8838  bren  8874  brdomg  8876  fundmen  8948  domssex  9046  mapen  9049  ssenen  9059  hartogslem1  9423  wemapso  9432  brwdomn0  9450  unxpwdom2  9469  ixpiunwdom  9471  oemapwe  9579  cantnffval2  9580  r0weon  9898  fseqenlem2  9911  acndom  9937  acndom2  9940  dfac9  10023  ackbij2lem2  10125  ackbij2lem3  10126  cfsmolem  10156  coftr  10159  dcomex  10333  axdc3lem4  10339  axdclem  10405  axdclem2  10406  fodomb  10412  brdom3  10414  brdom5  10415  brdom4  10416  shftfval  14972  prdsvallem  17353  isoval  17667  issubc  17737  prfval  18100  psgnghm2  21513  psdmul  22076  dfac14  23528  indishmph  23708  ufldom  23872  tsmsval2  24040  dvmptadd  25886  dvmptmul  25887  dvmptco  25898  taylfval  26288  usgrsizedg  29188  usgredgleordALT  29207  vtxdun  29455  vtxdlfgrval  29459  vtxd0nedgb  29462  vtxdushgrfvedglem  29463  vtxdushgrfvedg  29464  vtxdginducedm1lem4  29516  vtxdginducedm1  29517  ewlksfval  29575  wksfval  29583  wlkiswwlksupgr2  29850  vdn0conngrumgrv2  30168  vdgn1frgrv2  30268  hmoval  30782  cyc3conja  33118  esum2d  34098  sitmval  34354  bnj893  34932  fmlafv  35416  fmla  35417  fmlasuc0  35420  dfrecs2  35984  dfrdg4  35985  indexdom  37774  dibfval  41180  aomclem1  43087  dfac21  43099  trclexi  43653  rtrclexi  43654  dfrtrcl5  43662  dfrcl2  43707  dvsubf  45952  dvdivf  45960  fouriersw  46269  smflimlem1  46809  smflimlem6  46814  smfpimcc  46846  smfsuplem1  46849  smfinflem  46855  smflimsuplem1  46858  smflimsuplem2  46859  smflimsuplem3  46860  smflimsuplem4  46861  smflimsuplem5  46862  smflimsuplem7  46864  smfliminflem  46868  fsupdm  46880  finfdm  46884  grimidvtxedg  47916  isuspgrim0  47925  cycldlenngric  47959  upwlksfval  48166  dfinito4  49533  dftermo4  49534