Theorem dmex 7618

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

Syntax hints:   ∈ wcel 2114  Vcvv 3496  dom cdm 5557

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332  ax-un 7463

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-cnv 5565  df-dm 5567  df-rn 5568

This theorem is referenced by:  elxp4  7629  ofmres  7687  1stval  7693  fo1st  7711  frxp  7822  tfrlem8  8022  mapprc  8412  ixpprc  8485  bren  8520  brdomg  8521  fundmen  8585  domssex  8680  mapen  8683  ssenen  8693  hartogslem1  9008  brwdomn0  9035  unxpwdom2  9054  ixpiunwdom  9057  oemapwe  9159  cantnffval2  9160  r0weon  9440  fseqenlem2  9453  acndom  9479  acndom2  9482  dfac9  9564  ackbij2lem2  9664  ackbij2lem3  9665  cfsmolem  9694  coftr  9697  dcomex  9871  axdc3lem4  9877  axdclem  9943  axdclem2  9944  fodomb  9950  brdom3  9952  brdom5  9953  brdom4  9954  hashfacen  13815  shftfval  14431  prdsval  16730  isoval  17037  issubc  17107  prfval  17451  psgnghm2  20727  dfac14  22228  indishmph  22408  ufldom  22572  tsmsval2  22740  dvmptadd  24559  dvmptmul  24560  dvmptco  24571  taylfval  24949  usgrsizedg  26999  usgredgleordALT  27018  vtxdun  27265  vtxdlfgrval  27269  vtxd0nedgb  27272  vtxdushgrfvedglem  27273  vtxdushgrfvedg  27274  vtxdginducedm1lem4  27326  vtxdginducedm1  27327  ewlksfval  27385  wksfval  27393  wksv  27403  wlkiswwlksupgr2  27657  vdn0conngrumgrv2  27977  vdgn1frgrv2  28077  hmoval  28589  cyc3conja  30801  esum2d  31354  sitmval  31609  bnj893  32202  fmlafv  32629  fmla  32630  fmlasuc0  32633  dfrecs2  33413  dfrdg4  33414  indexdom  35011  dibfval  38279  aomclem1  39661  dfac21  39673  trclexi  39987  rtrclexi  39988  dfrtrcl5  39996  dfrcl2  40026  dvsubf  42205  dvdivf  42214  fouriersw  42523  smflimlem1  43054  smflimlem6  43059  smfpimcc  43089  smfsuplem1  43092  smfinflem  43098  smflimsuplem1  43101  smflimsuplem2  43102  smflimsuplem3  43103  smflimsuplem4  43104  smflimsuplem5  43105  smflimsuplem7  43107  smfliminflem  43111  upwlksfval  44017