Theorem dmex 7906

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3450  dom cdm 5655

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pr 5398  ax-un 7736

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-cnv 5663  df-dm 5665  df-rn 5666

This theorem is used by:  elxp4  7919  ofmres  7981  1stval  7988  fo1st  8006  frxp  8124  frxp2  8142  frxp3  8149  tfrlem8  8373  mapprc  8830  ixpprc  8926  bren  8962  brdomg  8964  fundmen  9038  domssex  9136  mapen  9139  ssenen  9149  hartogslem1  9514  wemapso  9523  brwdomn0  9541  unxpwdom2  9560  ixpiunwdom  9562  oemapwe  9673  cantnffval2  9674  r0weon  10015  fseqenlem2  10028  acndom  10054  acndom2  10057  dfac9  10139  ackbij2lem2  10241  ackbij2lem3  10242  cfsmolem  10272  coftr  10275  dcomex  10449  axdc3lem4  10455  axdclem  10521  axdclem2  10522  fodomb  10529  brdom3  10531  brdom5  10532  brdom4  10533  shftfval  15143  prdsvallem  17539  isoval  17854  issubc  17924  prfval  18287  psgnghm2  21794  psdmul  22394  dfac14  23844  indishmph  24024  ufldom  24188  tsmsval2  24356  dvmptadd  26187  dvmptmul  26188  dvmptco  26199  taylfval  26595  usgrsizedg  29675  usgredgleordALT  29694  vtxdun  29941  vtxdlfgrval  29945  vtxd0nedgb  29948  vtxdushgrfvedglem  29949  vtxdushgrfvedg  29950  vtxdginducedm1lem4  30002  vtxdginducedm1  30003  ewlksfval  30061  wksfval  30069  wlkiswwlksupgr2  30345  vdn0conngrumgrv2  30676  vdgn1frgrv2  30776  hmoval  31291  cyc3conja  33597  esum2d  34603  sitmval  34860  bnj893  35437  fmlafv  35959  fmla  35960  fmlasuc0  35963  dfrecs2  36529  dfrdg4  36530  indexdom  38484  dibfval  42014  aomclem1  43895  dfac21  43907  trclexi  44460  rtrclexi  44461  dfrtrcl5  44469  dfrcl2  44514  dvsubf  46742  dvdivf  46750  fouriersw  47059  smflimlem1  47599  smflimlem6  47604  smfpimcc  47636  smfsuplem1  47639  smfinflem  47645  smflimsuplem1  47648  smflimsuplem2  47649  smflimsuplem3  47650  smflimsuplem4  47651  smflimsuplem5  47652  smflimsuplem7  47654  smfliminflem  47658  fsupdm  47670  finfdm  47674  grimidvtxedg  48801  isuspgrim0  48810  cycldlenngric  48844  upwlksfval  49051  dfinito4  50427  dftermo4  50428