Theorem dmex 7853

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

Syntax hints:   ∈ wcel 2114  Vcvv 3430  dom cdm 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pr 5370  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-cnv 5632  df-dm 5634  df-rn 5635

This theorem is referenced by:  elxp4  7866  ofmres  7930  1stval  7937  fo1st  7955  frxp  8069  frxp2  8087  frxp3  8094  tfrlem8  8316  mapprc  8770  ixpprc  8860  bren  8896  brdomg  8898  fundmen  8971  domssex  9069  mapen  9072  ssenen  9082  hartogslem1  9450  wemapso  9459  brwdomn0  9477  unxpwdom2  9496  ixpiunwdom  9498  oemapwe  9606  cantnffval2  9607  r0weon  9925  fseqenlem2  9938  acndom  9964  acndom2  9967  dfac9  10050  ackbij2lem2  10152  ackbij2lem3  10153  cfsmolem  10183  coftr  10186  dcomex  10360  axdc3lem4  10366  axdclem  10432  axdclem2  10433  fodomb  10439  brdom3  10441  brdom5  10442  brdom4  10443  shftfval  15023  prdsvallem  17408  isoval  17723  issubc  17793  prfval  18156  psgnghm2  21571  psdmul  22142  dfac14  23593  indishmph  23773  ufldom  23937  tsmsval2  24105  dvmptadd  25937  dvmptmul  25938  dvmptco  25949  taylfval  26335  usgrsizedg  29298  usgredgleordALT  29317  vtxdun  29565  vtxdlfgrval  29569  vtxd0nedgb  29572  vtxdushgrfvedglem  29573  vtxdushgrfvedg  29574  vtxdginducedm1lem4  29626  vtxdginducedm1  29627  ewlksfval  29685  wksfval  29693  wlkiswwlksupgr2  29960  vdn0conngrumgrv2  30281  vdgn1frgrv2  30381  hmoval  30896  cyc3conja  33233  esum2d  34253  sitmval  34509  bnj893  35086  fmlafv  35578  fmla  35579  fmlasuc0  35582  dfrecs2  36148  dfrdg4  36149  indexdom  38069  dibfval  41601  aomclem1  43500  dfac21  43512  trclexi  44065  rtrclexi  44066  dfrtrcl5  44074  dfrcl2  44119  dvsubf  46360  dvdivf  46368  fouriersw  46677  smflimlem1  47217  smflimlem6  47222  smfpimcc  47254  smfsuplem1  47257  smfinflem  47263  smflimsuplem1  47266  smflimsuplem2  47267  smflimsuplem3  47268  smflimsuplem4  47269  smflimsuplem5  47270  smflimsuplem7  47272  smfliminflem  47276  fsupdm  47288  finfdm  47292  grimidvtxedg  48373  isuspgrim0  48382  cycldlenngric  48416  upwlksfval  48623  dfinito4  49988  dftermo4  49989