Theorem dmex 7907

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

Syntax hints:   ∈ wcel 2143  Vcvv 3455  dom cdm 5663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406  ax-un 7734

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-uni 4874  df-br 5111  df-opab 5175  df-cnv 5671  df-dm 5673  df-rn 5674

This theorem is referenced by:  elxp4  7920  ofmres  7982  1stval  7989  fo1st  8007  frxp  8123  frxp2  8141  frxp3  8148  tfrlem8  8372  mapprc  8829  ixpprc  8918  bren  8954  brdomg  8956  fundmen  9029  domssex  9127  mapen  9130  ssenen  9140  hartogslem1  9505  wemapso  9514  brwdomn0  9532  unxpwdom2  9551  ixpiunwdom  9553  oemapwe  9664  cantnffval2  9665  r0weon  9997  fseqenlem2  10010  acndom  10036  acndom2  10039  dfac9  10121  ackbij2lem2  10223  ackbij2lem3  10224  cfsmolem  10255  coftr  10258  dcomex  10432  axdc3lem4  10438  axdclem  10504  axdclem2  10505  fodomb  10511  brdom3  10513  brdom5  10514  brdom4  10515  shftfval  15109  prdsvallem  17508  isoval  17823  issubc  17893  prfval  18256  psgnghm2  21712  psdmul  22310  dfac14  23756  indishmph  23936  ufldom  24100  tsmsval2  24268  dvmptadd  26100  dvmptmul  26101  dvmptco  26112  taylfval  26503  usgrsizedg  29546  usgredgleordALT  29565  vtxdun  29812  vtxdlfgrval  29816  vtxd0nedgb  29819  vtxdushgrfvedglem  29820  vtxdushgrfvedg  29821  vtxdginducedm1lem4  29873  vtxdginducedm1  29874  ewlksfval  29932  wksfval  29940  wlkiswwlksupgr2  30207  vdn0conngrumgrv2  30528  vdgn1frgrv2  30628  hmoval  31143  cyc3conja  33458  esum2d  34464  sitmval  34720  bnj893  35297  fmlafv  35853  fmla  35854  fmlasuc0  35857  dfrecs2  36423  dfrdg4  36424  indexdom  38366  dibfval  41896  aomclem1  43764  dfac21  43776  trclexi  44329  rtrclexi  44330  dfrtrcl5  44338  dfrcl2  44383  dvsubf  46611  dvdivf  46619  fouriersw  46928  smflimlem1  47468  smflimlem6  47473  smfpimcc  47505  smfsuplem1  47508  smfinflem  47514  smflimsuplem1  47517  smflimsuplem2  47518  smflimsuplem3  47519  smflimsuplem4  47520  smflimsuplem5  47521  smflimsuplem7  47523  smfliminflem  47527  fsupdm  47539  finfdm  47543  grimidvtxedg  48633  isuspgrim0  48642  cycldlenngric  48676  upwlksfval  48883  dfinito4  50262  dftermo4  50263