Theorem dmex 7758

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

Syntax hints:   ∈ wcel 2106  Vcvv 3432  dom cdm 5589

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-cnv 5597  df-dm 5599  df-rn 5600

This theorem is referenced by:  elxp4  7769  ofmres  7827  1stval  7833  fo1st  7851  frxp  7967  tfrlem8  8215  mapprc  8619  ixpprc  8707  bren  8743  brenOLD  8744  brdomg  8746  brdomgOLD  8747  fundmen  8821  domssex  8925  mapen  8928  ssenen  8938  hartogslem1  9301  wemapso  9310  brwdomn0  9328  unxpwdom2  9347  ixpiunwdom  9349  oemapwe  9452  cantnffval2  9453  r0weon  9768  fseqenlem2  9781  acndom  9807  acndom2  9810  dfac9  9892  ackbij2lem2  9996  ackbij2lem3  9997  cfsmolem  10026  coftr  10029  dcomex  10203  axdc3lem4  10209  axdclem  10275  axdclem2  10276  fodomb  10282  brdom3  10284  brdom5  10285  brdom4  10286  hashfacenOLD  14167  shftfval  14781  prdsvallem  17165  isoval  17477  issubc  17550  prfval  17916  psgnghm2  20786  dfac14  22769  indishmph  22949  ufldom  23113  tsmsval2  23281  dvmptadd  25124  dvmptmul  25125  dvmptco  25136  taylfval  25518  usgrsizedg  27582  usgredgleordALT  27601  vtxdun  27848  vtxdlfgrval  27852  vtxd0nedgb  27855  vtxdushgrfvedglem  27856  vtxdushgrfvedg  27857  vtxdginducedm1lem4  27909  vtxdginducedm1  27910  ewlksfval  27968  wksfval  27976  wksvOLD  27987  wlkiswwlksupgr2  28242  vdn0conngrumgrv2  28560  vdgn1frgrv2  28660  hmoval  29172  cyc3conja  31424  esum2d  32061  sitmval  32316  bnj893  32908  fmlafv  33342  fmla  33343  fmlasuc0  33346  frxp2  33791  frxp3  33797  dfrecs2  34252  dfrdg4  34253  indexdom  35892  dibfval  39155  aomclem1  40879  dfac21  40891  trclexi  41228  rtrclexi  41229  dfrtrcl5  41237  dfrcl2  41282  dvsubf  43455  dvdivf  43463  fouriersw  43772  smflimlem1  44306  smflimlem6  44311  smfpimcc  44341  smfsuplem1  44344  smfinflem  44350  smflimsuplem1  44353  smflimsuplem2  44354  smflimsuplem3  44355  smflimsuplem4  44356  smflimsuplem5  44357  smflimsuplem7  44359  smfliminflem  44363  upwlksfval  45297