Theorem dmex 7908

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

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3457  dom cdm 5663

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406  ax-un 7738

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-cnv 5671  df-dm 5673  df-rn 5674

This theorem is used by:  elxp4  7921  ofmres  7983  1stval  7990  fo1st  8008  frxp  8124  frxp2  8142  frxp3  8149  tfrlem8  8373  mapprc  8830  ixpprc  8919  bren  8955  brdomg  8957  fundmen  9031  domssex  9129  mapen  9132  ssenen  9142  hartogslem1  9507  wemapso  9516  brwdomn0  9534  unxpwdom2  9553  ixpiunwdom  9555  oemapwe  9666  cantnffval2  9667  r0weon  10008  fseqenlem2  10021  acndom  10047  acndom2  10050  dfac9  10132  ackbij2lem2  10234  ackbij2lem3  10235  cfsmolem  10265  coftr  10268  dcomex  10442  axdc3lem4  10448  axdclem  10514  axdclem2  10515  fodomb  10521  brdom3  10523  brdom5  10524  brdom4  10525  shftfval  15126  prdsvallem  17524  isoval  17839  issubc  17909  prfval  18272  psgnghm2  21760  psdmul  22358  dfac14  23804  indishmph  23984  ufldom  24148  tsmsval2  24316  dvmptadd  26148  dvmptmul  26149  dvmptco  26160  taylfval  26551  usgrsizedg  29594  usgredgleordALT  29613  vtxdun  29860  vtxdlfgrval  29864  vtxd0nedgb  29867  vtxdushgrfvedglem  29868  vtxdushgrfvedg  29869  vtxdginducedm1lem4  29921  vtxdginducedm1  29922  ewlksfval  29980  wksfval  29988  wlkiswwlksupgr2  30255  vdn0conngrumgrv2  30576  vdgn1frgrv2  30676  hmoval  31191  cyc3conja  33500  esum2d  34506  sitmval  34763  bnj893  35340  fmlafv  35885  fmla  35886  fmlasuc0  35889  dfrecs2  36455  dfrdg4  36456  indexdom  38418  dibfval  41948  aomclem1  43814  dfac21  43826  trclexi  44379  rtrclexi  44380  dfrtrcl5  44388  dfrcl2  44433  dvsubf  46661  dvdivf  46669  fouriersw  46978  smflimlem1  47518  smflimlem6  47523  smfpimcc  47555  smfsuplem1  47558  smfinflem  47564  smflimsuplem1  47567  smflimsuplem2  47568  smflimsuplem3  47569  smflimsuplem4  47570  smflimsuplem5  47571  smflimsuplem7  47573  smfliminflem  47577  fsupdm  47589  finfdm  47593  grimidvtxedg  48683  isuspgrim0  48692  cycldlenngric  48726  upwlksfval  48933  dfinito4  50312  dftermo4  50313