Theorem dmex 7955

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

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454  dom cdm 5658

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pr 5398  ax-un 7783

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-cnv 5666  df-dm 5668  df-rn 5669

This theorem is used by:  elxp4  7968  ofmres  8030  1stval  8037  fo1st  8055  frxp  8175  frxp2  8198  frxp3  8205  tfrlem8  8430  mapprc  8889  ixpprc  8985  bren  9021  brdomg  9023  fundmen  9097  domssex  9195  mapen  9198  ssenen  9208  hartogslem1  9573  wemapso  9582  brwdomn0  9600  unxpwdom2  9619  ixpiunwdom  9621  oemapwe  9732  cantnffval2  9733  r0weon  10130  fseqenlem2  10143  acndom  10169  acndom2  10172  dfac9  10254  ackbij2lem2  10356  ackbij2lem3  10357  cfsmolem  10387  coftr  10390  dcomex  10564  axdc3lem4  10570  axdclem  10636  axdclem2  10637  fodomb  10644  brdom3  10646  brdom5  10647  brdom4  10648  shftfval  15266  prdsvallem  17675  isoval  17990  issubc  18060  prfval  18423  psgnghm2  21942  psdmul  22542  dfac14  23992  indishmph  24172  ufldom  24336  tsmsval2  24504  dvmptadd  26335  dvmptmul  26336  dvmptco  26347  taylfval  26743  usgrsizedg  29853  usgredgleordALT  29872  vtxdun  30119  vtxdlfgrval  30123  vtxd0nedgb  30126  vtxdushgrfvedglem  30127  vtxdushgrfvedg  30128  vtxdginducedm1lem4  30180  vtxdginducedm1  30181  ewlksfval  30239  wksfval  30247  wlkiswwlksupgr2  30523  vdn0conngrumgrv2  30854  vdgn1frgrv2  30954  hmoval  31469  cyc3conja  33817  esum2d  34836  sitmval  35092  bnj893  35669  fmlafv  36353  fmla  36354  fmlasuc0  36357  dfrecs2  36929  dfrdg4  36930  indexdom  38936  dibfval  42464  aomclem1  44322  dfac21  44334  trclexi  44881  rtrclexi  44882  dfrtrcl5  44890  dfrcl2  44935  dvsubf  47197  dvdivf  47205  fouriersw  47514  smflimlem1  48054  smflimlem6  48059  smfpimcc  48091  smfsuplem1  48094  smfinflem  48100  smflimsuplem1  48103  smflimsuplem2  48104  smflimsuplem3  48105  smflimsuplem4  48106  smflimsuplem5  48107  smflimsuplem7  48109  smfliminflem  48113  fsupdm  48125  finfdm  48129  grimidvtxedg  49256  isuspgrim0  49265  cycldlenngric  49299  upwlksfval  49506  dfinito4  50967  dftermo4  50968