Theorem dmex 7654

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

Syntax hints:   ∈ wcel 2114  Vcvv 3400  dom cdm 5535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2711  ax-sep 5177  ax-nul 5184  ax-pr 5306  ax-un 7491

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-rab 3063  df-v 3402  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4222  df-if 4425  df-sn 4527  df-pr 4529  df-op 4533  df-uni 4807  df-br 5041  df-opab 5103  df-cnv 5543  df-dm 5545  df-rn 5546

This theorem is referenced by:  elxp4  7665  ofmres  7722  1stval  7728  fo1st  7746  frxp  7858  tfrlem8  8061  mapprc  8453  ixpprc  8541  bren  8576  brdomg  8577  fundmen  8642  domssex  8740  mapen  8743  ssenen  8753  hartogslem1  9091  wemapso  9100  brwdomn0  9118  unxpwdom2  9137  ixpiunwdom  9139  oemapwe  9242  cantnffval2  9243  r0weon  9524  fseqenlem2  9537  acndom  9563  acndom2  9566  dfac9  9648  ackbij2lem2  9752  ackbij2lem3  9753  cfsmolem  9782  coftr  9785  dcomex  9959  axdc3lem4  9965  axdclem  10031  axdclem2  10032  fodomb  10038  brdom3  10040  brdom5  10041  brdom4  10042  hashfacenOLD  13917  shftfval  14531  prdsval  16843  isoval  17152  issubc  17222  prfval  17577  psgnghm2  20409  dfac14  22381  indishmph  22561  ufldom  22725  tsmsval2  22893  dvmptadd  24724  dvmptmul  24725  dvmptco  24736  taylfval  25118  usgrsizedg  27169  usgredgleordALT  27188  vtxdun  27435  vtxdlfgrval  27439  vtxd0nedgb  27442  vtxdushgrfvedglem  27443  vtxdushgrfvedg  27444  vtxdginducedm1lem4  27496  vtxdginducedm1  27497  ewlksfval  27555  wksfval  27563  wksv  27573  wlkiswwlksupgr2  27827  vdn0conngrumgrv2  28145  vdgn1frgrv2  28245  hmoval  28757  cyc3conja  31013  esum2d  31643  sitmval  31898  bnj893  32491  fmlafv  32925  fmla  32926  fmlasuc0  32929  frxp2  33416  frxp3  33422  dfrecs2  33907  dfrdg4  33908  indexdom  35547  dibfval  38810  aomclem1  40491  dfac21  40503  trclexi  40813  rtrclexi  40814  dfrtrcl5  40822  dfrcl2  40868  dvsubf  43037  dvdivf  43045  fouriersw  43354  smflimlem1  43885  smflimlem6  43890  smfpimcc  43920  smfsuplem1  43923  smfinflem  43929  smflimsuplem1  43932  smflimsuplem2  43933  smflimsuplem3  43934  smflimsuplem4  43935  smflimsuplem5  43936  smflimsuplem7  43938  smfliminflem  43942  upwlksfval  44878