Theorem dmex 7849

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

Syntax hints:   ∈ wcel 2109  Vcvv 3438  dom cdm 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7675

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-cnv 5631  df-dm 5633  df-rn 5634

This theorem is referenced by:  elxp4  7862  ofmres  7926  1stval  7933  fo1st  7951  frxp  8066  frxp2  8084  frxp3  8091  tfrlem8  8313  mapprc  8764  ixpprc  8853  bren  8889  brdomg  8891  fundmen  8963  domssex  9062  mapen  9065  ssenen  9075  hartogslem1  9453  wemapso  9462  brwdomn0  9480  unxpwdom2  9499  ixpiunwdom  9501  oemapwe  9609  cantnffval2  9610  r0weon  9925  fseqenlem2  9938  acndom  9964  acndom2  9967  dfac9  10050  ackbij2lem2  10152  ackbij2lem3  10153  cfsmolem  10183  coftr  10186  dcomex  10360  axdc3lem4  10366  axdclem  10432  axdclem2  10433  fodomb  10439  brdom3  10441  brdom5  10442  brdom4  10443  shftfval  14995  prdsvallem  17376  isoval  17690  issubc  17760  prfval  18123  psgnghm2  21506  psdmul  22069  dfac14  23521  indishmph  23701  ufldom  23865  tsmsval2  24033  dvmptadd  25880  dvmptmul  25881  dvmptco  25892  taylfval  26282  usgrsizedg  29178  usgredgleordALT  29197  vtxdun  29445  vtxdlfgrval  29449  vtxd0nedgb  29452  vtxdushgrfvedglem  29453  vtxdushgrfvedg  29454  vtxdginducedm1lem4  29506  vtxdginducedm1  29507  ewlksfval  29565  wksfval  29573  wlkiswwlksupgr2  29840  vdn0conngrumgrv2  30158  vdgn1frgrv2  30258  hmoval  30772  cyc3conja  33112  esum2d  34062  sitmval  34319  bnj893  34897  fmlafv  35355  fmla  35356  fmlasuc0  35359  dfrecs2  35926  dfrdg4  35927  indexdom  37716  dibfval  41123  aomclem1  43030  dfac21  43042  trclexi  43596  rtrclexi  43597  dfrtrcl5  43605  dfrcl2  43650  dvsubf  45899  dvdivf  45907  fouriersw  46216  smflimlem1  46756  smflimlem6  46761  smfpimcc  46793  smfsuplem1  46796  smfinflem  46802  smflimsuplem1  46805  smflimsuplem2  46806  smflimsuplem3  46807  smflimsuplem4  46808  smflimsuplem5  46809  smflimsuplem7  46811  smfliminflem  46815  fsupdm  46827  finfdm  46831  grimidvtxedg  47873  isuspgrim0  47882  cycldlenngric  47916  upwlksfval  48123  dfinito4  49490  dftermo4  49491