Theorem dmex 7851

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

Syntax hints:   ∈ wcel 2113  Vcvv 3440  dom cdm 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-cnv 5632  df-dm 5634  df-rn 5635

This theorem is referenced by:  elxp4  7864  ofmres  7928  1stval  7935  fo1st  7953  frxp  8068  frxp2  8086  frxp3  8093  tfrlem8  8315  mapprc  8767  ixpprc  8857  bren  8893  brdomg  8895  fundmen  8968  domssex  9066  mapen  9069  ssenen  9079  hartogslem1  9447  wemapso  9456  brwdomn0  9474  unxpwdom2  9493  ixpiunwdom  9495  oemapwe  9603  cantnffval2  9604  r0weon  9922  fseqenlem2  9935  acndom  9961  acndom2  9964  dfac9  10047  ackbij2lem2  10149  ackbij2lem3  10150  cfsmolem  10180  coftr  10183  dcomex  10357  axdc3lem4  10363  axdclem  10429  axdclem2  10430  fodomb  10436  brdom3  10438  brdom5  10439  brdom4  10440  shftfval  14993  prdsvallem  17374  isoval  17689  issubc  17759  prfval  18122  psgnghm2  21536  psdmul  22109  dfac14  23562  indishmph  23742  ufldom  23906  tsmsval2  24074  dvmptadd  25920  dvmptmul  25921  dvmptco  25932  taylfval  26322  usgrsizedg  29288  usgredgleordALT  29307  vtxdun  29555  vtxdlfgrval  29559  vtxd0nedgb  29562  vtxdushgrfvedglem  29563  vtxdushgrfvedg  29564  vtxdginducedm1lem4  29616  vtxdginducedm1  29617  ewlksfval  29675  wksfval  29683  wlkiswwlksupgr2  29950  vdn0conngrumgrv2  30271  vdgn1frgrv2  30371  hmoval  30885  cyc3conja  33239  esum2d  34250  sitmval  34506  bnj893  35084  fmlafv  35574  fmla  35575  fmlasuc0  35578  dfrecs2  36144  dfrdg4  36145  indexdom  37935  dibfval  41401  aomclem1  43296  dfac21  43308  trclexi  43861  rtrclexi  43862  dfrtrcl5  43870  dfrcl2  43915  dvsubf  46158  dvdivf  46166  fouriersw  46475  smflimlem1  47015  smflimlem6  47020  smfpimcc  47052  smfsuplem1  47055  smfinflem  47061  smflimsuplem1  47064  smflimsuplem2  47065  smflimsuplem3  47066  smflimsuplem4  47067  smflimsuplem5  47068  smflimsuplem7  47070  smfliminflem  47074  fsupdm  47086  finfdm  47090  grimidvtxedg  48131  isuspgrim0  48140  cycldlenngric  48174  upwlksfval  48381  dfinito4  49746  dftermo4  49747