Theorem dmex 7360

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

Syntax hints:   ∈ wcel 2166  Vcvv 3413  dom cdm 5341

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2390  ax-ext 2802  ax-sep 5004  ax-nul 5012  ax-pr 5126  ax-un 7208

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2604  df-eu 2639  df-clab 2811  df-cleq 2817  df-clel 2820  df-nfc 2957  df-rex 3122  df-rab 3125  df-v 3415  df-dif 3800  df-un 3802  df-in 3804  df-ss 3811  df-nul 4144  df-if 4306  df-sn 4397  df-pr 4399  df-op 4403  df-uni 4658  df-br 4873  df-opab 4935  df-cnv 5349  df-dm 5351  df-rn 5352

This theorem is referenced by:  elxp4  7371  ofmres  7423  1stval  7429  fo1st  7447  frxp  7550  tfrlem8  7745  mapprc  8125  ixpprc  8195  bren  8230  brdomg  8231  ctex  8236  fundmen  8295  domssex  8389  mapen  8392  ssenen  8402  hartogslem1  8715  brwdomn0  8742  unxpwdom2  8761  ixpiunwdom  8764  oemapwe  8867  cantnffval2  8868  r0weon  9147  fseqenlem2  9160  acndom  9186  acndom2  9189  dfac9  9272  ackbij2lem2  9376  ackbij2lem3  9377  cfsmolem  9406  coftr  9409  dcomex  9583  axdc3lem4  9589  axdclem  9655  axdclem2  9656  fodomb  9662  brdom3  9664  brdom5  9665  brdom4  9666  hashfacen  13526  shftfval  14186  prdsval  16467  isoval  16776  issubc  16846  prfval  17191  symgbas  18149  psgnghm2  20285  dfac14  21791  indishmph  21971  ufldom  22135  tsmsval2  22302  dvmptadd  24121  dvmptmul  24122  dvmptco  24133  taylfval  24511  usgrsizedg  26510  usgredgleordALT  26530  vtxdun  26778  vtxdlfgrval  26782  vtxd0nedgb  26785  vtxdushgrfvedglem  26786  vtxdushgrfvedg  26787  vtxdginducedm1lem4  26839  vtxdginducedm1  26840  ewlksfval  26898  wksfval  26906  wksv  26916  wlkiswwlksupgr2  27175  vdn0conngrumgrv2  27571  vdgn1frgrv2  27676  hmoval  28219  esum2d  30699  sitmval  30955  bnj893  31543  dfrecs2  32595  dfrdg4  32596  cnfinltrel  33785  indexdom  34071  dibfval  37215  aomclem1  38466  dfac21  38478  trclexi  38767  rtrclexi  38768  dfrtrcl5  38776  dfrcl2  38806  dvsubf  40922  dvdivf  40931  fouriersw  41241  smflimlem1  41772  smflimlem6  41777  smfpimcc  41807  smfsuplem1  41810  smfinflem  41816  smflimsuplem1  41819  smflimsuplem2  41820  smflimsuplem3  41821  smflimsuplem4  41822  smflimsuplem5  41823  smflimsuplem7  41825  smfliminflem  41829  upwlksfval  42562