Theorem dmex 7899

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

Syntax hints:   ∈ wcel 2107  Vcvv 3457  dom cdm 5651

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706  ax-sep 5263  ax-nul 5273  ax-pr 5399  ax-un 7723

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3414  df-v 3459  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-nul 4307  df-if 4499  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4881  df-br 5117  df-opab 5179  df-cnv 5659  df-dm 5661  df-rn 5662

This theorem is referenced by:  elxp4  7912  ofmres  7977  1stval  7984  fo1st  8002  frxp  8119  frxp2  8137  frxp3  8144  tfrlem8  8392  mapprc  8838  ixpprc  8927  bren  8963  brdomg  8965  brdomgOLD  8966  fundmen  9039  domssex  9146  mapen  9149  ssenen  9159  hartogslem1  9548  wemapso  9557  brwdomn0  9575  unxpwdom2  9594  ixpiunwdom  9596  oemapwe  9700  cantnffval2  9701  r0weon  10018  fseqenlem2  10031  acndom  10057  acndom2  10060  dfac9  10143  ackbij2lem2  10245  ackbij2lem3  10246  cfsmolem  10276  coftr  10279  dcomex  10453  axdc3lem4  10459  axdclem  10525  axdclem2  10526  fodomb  10532  brdom3  10534  brdom5  10535  brdom4  10536  shftfval  15076  prdsvallem  17453  isoval  17763  issubc  17833  prfval  18196  psgnghm2  21526  psdmul  22089  dfac14  23541  indishmph  23721  ufldom  23885  tsmsval2  24053  dvmptadd  25901  dvmptmul  25902  dvmptco  25913  taylfval  26303  usgrsizedg  29126  usgredgleordALT  29145  vtxdun  29393  vtxdlfgrval  29397  vtxd0nedgb  29400  vtxdushgrfvedglem  29401  vtxdushgrfvedg  29402  vtxdginducedm1lem4  29454  vtxdginducedm1  29455  ewlksfval  29513  wksfval  29521  wksvOLD  29532  wlkiswwlksupgr2  29791  vdn0conngrumgrv2  30109  vdgn1frgrv2  30209  hmoval  30723  cyc3conja  33086  esum2d  34032  sitmval  34289  bnj893  34880  fmlafv  35323  fmla  35324  fmlasuc0  35327  dfrecs2  35889  dfrdg4  35890  indexdom  37679  dibfval  41081  aomclem1  43003  dfac21  43015  trclexi  43569  rtrclexi  43570  dfrtrcl5  43578  dfrcl2  43623  dvsubf  45873  dvdivf  45881  fouriersw  46190  smflimlem1  46730  smflimlem6  46735  smfpimcc  46767  smfsuplem1  46770  smfinflem  46776  smflimsuplem1  46779  smflimsuplem2  46780  smflimsuplem3  46781  smflimsuplem4  46782  smflimsuplem5  46783  smflimsuplem7  46785  smfliminflem  46789  fsupdm  46801  finfdm  46805  isuspgrim0  47817  grimidvtxedg  47821  upwlksfval  47996  dfinito4  49171  dftermo4  49172