Theorem dmex 7885

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

Syntax hints:   ∈ wcel 2141  Vcvv 3453  dom cdm 5643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5243  ax-pr 5387  ax-un 7713

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-cnv 5651  df-dm 5653  df-rn 5654

This theorem is referenced by:  elxp4  7898  ofmres  7960  1stval  7967  fo1st  7985  frxp  8100  frxp2  8118  frxp3  8125  tfrlem8  8349  mapprc  8806  ixpprc  8895  bren  8931  brdomg  8933  fundmen  9006  domssex  9104  mapen  9107  ssenen  9117  hartogslem1  9484  wemapso  9493  brwdomn0  9511  unxpwdom2  9530  ixpiunwdom  9532  oemapwe  9643  cantnffval2  9644  r0weon  9962  fseqenlem2  9975  acndom  10001  acndom2  10004  dfac9  10087  ackbij2lem2  10189  ackbij2lem3  10190  cfsmolem  10221  coftr  10224  dcomex  10398  axdc3lem4  10404  axdclem  10470  axdclem2  10471  fodomb  10477  brdom3  10479  brdom5  10480  brdom4  10481  shftfval  15077  prdsvallem  17474  isoval  17789  issubc  17859  prfval  18222  psgnghm2  21621  psdmul  22219  dfac14  23666  indishmph  23846  ufldom  24010  tsmsval2  24178  dvmptadd  26010  dvmptmul  26011  dvmptco  26022  taylfval  26410  usgrsizedg  29373  usgredgleordALT  29392  vtxdun  29639  vtxdlfgrval  29643  vtxd0nedgb  29646  vtxdushgrfvedglem  29647  vtxdushgrfvedg  29648  vtxdginducedm1lem4  29700  vtxdginducedm1  29701  ewlksfval  29759  wksfval  29767  wlkiswwlksupgr2  30034  vdn0conngrumgrv2  30355  vdgn1frgrv2  30455  hmoval  30970  cyc3conja  33298  esum2d  34351  sitmval  34607  bnj893  35184  fmlafv  35691  fmla  35692  fmlasuc0  35695  dfrecs2  36261  dfrdg4  36262  indexdom  38194  dibfval  41726  aomclem1  43592  dfac21  43604  trclexi  44157  rtrclexi  44158  dfrtrcl5  44166  dfrcl2  44211  dvsubf  46449  dvdivf  46457  fouriersw  46766  smflimlem1  47306  smflimlem6  47311  smfpimcc  47343  smfsuplem1  47346  smfinflem  47352  smflimsuplem1  47355  smflimsuplem2  47356  smflimsuplem3  47357  smflimsuplem4  47358  smflimsuplem5  47359  smflimsuplem7  47361  smfliminflem  47365  fsupdm  47377  finfdm  47381  grimidvtxedg  48468  isuspgrim0  48477  cycldlenngric  48511  upwlksfval  48718  dfinito4  50083  dftermo4  50084