Theorem dmex 7885

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

Syntax hints:   ∈ wcel 2109  Vcvv 3447  dom cdm 5638

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-cnv 5646  df-dm 5648  df-rn 5649

This theorem is referenced by:  elxp4  7898  ofmres  7963  1stval  7970  fo1st  7988  frxp  8105  frxp2  8123  frxp3  8130  tfrlem8  8352  mapprc  8803  ixpprc  8892  bren  8928  brdomg  8930  fundmen  9002  domssex  9102  mapen  9105  ssenen  9115  hartogslem1  9495  wemapso  9504  brwdomn0  9522  unxpwdom2  9541  ixpiunwdom  9543  oemapwe  9647  cantnffval2  9648  r0weon  9965  fseqenlem2  9978  acndom  10004  acndom2  10007  dfac9  10090  ackbij2lem2  10192  ackbij2lem3  10193  cfsmolem  10223  coftr  10226  dcomex  10400  axdc3lem4  10406  axdclem  10472  axdclem2  10473  fodomb  10479  brdom3  10481  brdom5  10482  brdom4  10483  shftfval  15036  prdsvallem  17417  isoval  17727  issubc  17797  prfval  18160  psgnghm2  21490  psdmul  22053  dfac14  23505  indishmph  23685  ufldom  23849  tsmsval2  24017  dvmptadd  25864  dvmptmul  25865  dvmptco  25876  taylfval  26266  usgrsizedg  29142  usgredgleordALT  29161  vtxdun  29409  vtxdlfgrval  29413  vtxd0nedgb  29416  vtxdushgrfvedglem  29417  vtxdushgrfvedg  29418  vtxdginducedm1lem4  29470  vtxdginducedm1  29471  ewlksfval  29529  wksfval  29537  wksvOLD  29548  wlkiswwlksupgr2  29807  vdn0conngrumgrv2  30125  vdgn1frgrv2  30225  hmoval  30739  cyc3conja  33114  esum2d  34083  sitmval  34340  bnj893  34918  fmlafv  35367  fmla  35368  fmlasuc0  35371  dfrecs2  35938  dfrdg4  35939  indexdom  37728  dibfval  41135  aomclem1  43043  dfac21  43055  trclexi  43609  rtrclexi  43610  dfrtrcl5  43618  dfrcl2  43663  dvsubf  45912  dvdivf  45920  fouriersw  46229  smflimlem1  46769  smflimlem6  46774  smfpimcc  46806  smfsuplem1  46809  smfinflem  46815  smflimsuplem1  46818  smflimsuplem2  46819  smflimsuplem3  46820  smflimsuplem4  46821  smflimsuplem5  46822  smflimsuplem7  46824  smfliminflem  46828  fsupdm  46840  finfdm  46844  grimidvtxedg  47885  isuspgrim0  47894  cycldlenngric  47928  upwlksfval  48123  dfinito4  49490  dftermo4  49491