Theorem dmex 7897

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

Syntax hints:   ∈ wcel 2107  Vcvv 3475  dom cdm 5675

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7720

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-cnv 5683  df-dm 5685  df-rn 5686

This theorem is referenced by:  elxp4  7908  ofmres  7966  1stval  7972  fo1st  7990  frxp  8107  frxp2  8125  frxp3  8132  tfrlem8  8379  mapprc  8820  ixpprc  8909  bren  8945  brenOLD  8946  brdomg  8948  brdomgOLD  8949  fundmen  9027  domssex  9134  mapen  9137  ssenen  9147  hartogslem1  9533  wemapso  9542  brwdomn0  9560  unxpwdom2  9579  ixpiunwdom  9581  oemapwe  9685  cantnffval2  9686  r0weon  10003  fseqenlem2  10016  acndom  10042  acndom2  10045  dfac9  10127  ackbij2lem2  10231  ackbij2lem3  10232  cfsmolem  10261  coftr  10264  dcomex  10438  axdc3lem4  10444  axdclem  10510  axdclem2  10511  fodomb  10517  brdom3  10519  brdom5  10520  brdom4  10521  hashfacenOLD  14410  shftfval  15013  prdsvallem  17396  isoval  17708  issubc  17781  prfval  18147  psgnghm2  21118  dfac14  23104  indishmph  23284  ufldom  23448  tsmsval2  23616  dvmptadd  25459  dvmptmul  25460  dvmptco  25471  taylfval  25853  usgrsizedg  28452  usgredgleordALT  28471  vtxdun  28718  vtxdlfgrval  28722  vtxd0nedgb  28725  vtxdushgrfvedglem  28726  vtxdushgrfvedg  28727  vtxdginducedm1lem4  28779  vtxdginducedm1  28780  ewlksfval  28838  wksfval  28846  wksvOLD  28857  wlkiswwlksupgr2  29111  vdn0conngrumgrv2  29429  vdgn1frgrv2  29529  hmoval  30041  cyc3conja  32294  esum2d  33029  sitmval  33286  bnj893  33877  fmlafv  34309  fmla  34310  fmlasuc0  34313  dfrecs2  34860  dfrdg4  34861  indexdom  36540  dibfval  39950  aomclem1  41729  dfac21  41741  trclexi  42304  rtrclexi  42305  dfrtrcl5  42313  dfrcl2  42358  dvsubf  44565  dvdivf  44573  fouriersw  44882  smflimlem1  45422  smflimlem6  45427  smfpimcc  45459  smfsuplem1  45462  smfinflem  45468  smflimsuplem1  45471  smflimsuplem2  45472  smflimsuplem3  45473  smflimsuplem4  45474  smflimsuplem5  45475  smflimsuplem7  45477  smfliminflem  45481  fsupdm  45493  finfdm  45497  upwlksfval  46448