Theorem dmex 7919

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451  dom cdm 5651

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 2733  ax-sep 5249  ax-pr 5391  ax-un 7749

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  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 5659  df-dm 5661  df-rn 5662

This theorem is used by:  elxp4  7932  ofmres  7994  1stval  8001  fo1st  8019  frxp  8136  frxp2  8154  frxp3  8161  tfrlem8  8385  mapprc  8844  ixpprc  8940  bren  8976  brdomg  8978  fundmen  9052  domssex  9150  mapen  9153  ssenen  9163  hartogslem1  9529  wemapso  9538  brwdomn0  9556  unxpwdom2  9575  ixpiunwdom  9577  oemapwe  9688  cantnffval2  9689  r0weon  10084  fseqenlem2  10097  acndom  10123  acndom2  10126  dfac9  10208  ackbij2lem2  10310  ackbij2lem3  10311  cfsmolem  10341  coftr  10344  dcomex  10518  axdc3lem4  10524  axdclem  10590  axdclem2  10591  fodomb  10598  brdom3  10600  brdom5  10601  brdom4  10602  shftfval  15216  prdsvallem  17618  isoval  17933  issubc  18003  prfval  18366  psgnghm2  21880  psdmul  22480  dfac14  23930  indishmph  24110  ufldom  24274  tsmsval2  24442  dvmptadd  26273  dvmptmul  26274  dvmptco  26285  taylfval  26679  usgrsizedg  29789  usgredgleordALT  29808  vtxdun  30055  vtxdlfgrval  30059  vtxd0nedgb  30062  vtxdushgrfvedglem  30063  vtxdushgrfvedg  30064  vtxdginducedm1lem4  30116  vtxdginducedm1  30117  ewlksfval  30175  wksfval  30183  wlkiswwlksupgr2  30459  vdn0conngrumgrv2  30790  vdgn1frgrv2  30890  hmoval  31405  cyc3conja  33711  esum2d  34718  sitmval  34974  bnj893  35551  fmlafv  36124  fmla  36125  fmlasuc0  36128  dfrecs2  36694  dfrdg4  36695  indexdom  38648  dibfval  42178  aomclem1  44040  dfac21  44052  trclexi  44605  rtrclexi  44606  dfrtrcl5  44614  dfrcl2  44659  dvsubf  46893  dvdivf  46901  fouriersw  47210  smflimlem1  47750  smflimlem6  47755  smfpimcc  47787  smfsuplem1  47790  smfinflem  47796  smflimsuplem1  47799  smflimsuplem2  47800  smflimsuplem3  47801  smflimsuplem4  47802  smflimsuplem5  47803  smflimsuplem7  47805  smfliminflem  47809  fsupdm  47821  finfdm  47825  grimidvtxedg  48952  isuspgrim0  48961  cycldlenngric  48995  upwlksfval  49202  dfinito4  50578  dftermo4  50579