Theorem dmex 6991

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

Syntax hints:   ∈ wcel 1977  Vcvv 3173  dom cdm 5038

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-cnv 5046  df-dm 5048  df-rn 5049

This theorem is referenced by:  elxp4  7003  ofmres  7055  1stval  7061  fo1st  7079  frxp  7174  tfrlem8  7367  mapprc  7748  ixpprc  7815  bren  7850  brdomg  7851  ctex  7856  fundmen  7916  domssex  8006  mapen  8009  ssenen  8019  hartogslem1  8330  brwdomn0  8357  unxpwdom2  8376  ixpiunwdom  8379  oemapwe  8474  cantnffval2  8475  r0weon  8718  fseqenlem2  8731  acndom  8757  acndom2  8760  dfac9  8841  ackbij2lem2  8945  ackbij2lem3  8946  cfsmolem  8975  coftr  8978  dcomex  9152  axdc3lem4  9158  axdclem  9224  axdclem2  9225  fodomb  9229  brdom3  9231  brdom5  9232  brdom4  9233  hashfacen  13095  shftfval  13658  prdsval  15938  isoval  16248  issubc  16318  prfval  16662  symgbas  17623  psgnghm2  19746  dfac14  21231  indishmph  21411  ufldom  21576  tsmsval2  21743  dvmptadd  23529  dvmptmul  23530  dvmptco  23541  taylfval  23917  hmoval  27049  esum2d  29482  sitmval  29738  bnj893  30252  dfrecs2  31227  dfrdg4  31228  indexdom  32699  dibfval  35448  aomclem1  36642  dfac21  36654  trclexi  36946  rtrclexi  36947  dfrtrcl5  36955  dfrcl2  36985  dvsubf  38802  dvdivf  38812  fouriersw  39124  smflimlem1  39657  smflimlem6  39662  usgrsizedg  40442  usgredgaleordALT  40461  vtxdun  40696  vtxdlfgrval  40700  vtxd0nedgb  40703  vtxdushgrfvedglem  40704  vtxdushgrfvedg  40705  ewlksfval  40803  1wlksfval  40811  wlksfval  40812  1wlksv  40824  1wlkiswwlksupgr2  41074  vdn0conngrumgrv2  41363  vdgn1frgrv2  41466