Theorem dmex 7598

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

Syntax hints:   ∈ wcel 2111  Vcvv 3441  dom cdm 5519

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-cnv 5527  df-dm 5529  df-rn 5530

This theorem is referenced by:  elxp4  7609  ofmres  7667  1stval  7673  fo1st  7691  frxp  7803  tfrlem8  8003  mapprc  8393  ixpprc  8466  bren  8501  brdomg  8502  fundmen  8566  domssex  8662  mapen  8665  ssenen  8675  hartogslem1  8990  brwdomn0  9017  unxpwdom2  9036  ixpiunwdom  9038  oemapwe  9141  cantnffval2  9142  r0weon  9423  fseqenlem2  9436  acndom  9462  acndom2  9465  dfac9  9547  ackbij2lem2  9651  ackbij2lem3  9652  cfsmolem  9681  coftr  9684  dcomex  9858  axdc3lem4  9864  axdclem  9930  axdclem2  9931  fodomb  9937  brdom3  9939  brdom5  9940  brdom4  9941  hashfacen  13808  shftfval  14421  prdsval  16720  isoval  17027  issubc  17097  prfval  17441  psgnghm2  20270  dfac14  22223  indishmph  22403  ufldom  22567  tsmsval2  22735  dvmptadd  24563  dvmptmul  24564  dvmptco  24575  taylfval  24954  usgrsizedg  27005  usgredgleordALT  27024  vtxdun  27271  vtxdlfgrval  27275  vtxd0nedgb  27278  vtxdushgrfvedglem  27279  vtxdushgrfvedg  27280  vtxdginducedm1lem4  27332  vtxdginducedm1  27333  ewlksfval  27391  wksfval  27399  wksv  27409  wlkiswwlksupgr2  27663  vdn0conngrumgrv2  27981  vdgn1frgrv2  28081  hmoval  28593  cyc3conja  30849  esum2d  31462  sitmval  31717  bnj893  32310  fmlafv  32740  fmla  32741  fmlasuc0  32744  dfrecs2  33524  dfrdg4  33525  indexdom  35172  dibfval  38437  aomclem1  39998  dfac21  40010  trclexi  40320  rtrclexi  40321  dfrtrcl5  40329  dfrcl2  40375  dvsubf  42556  dvdivf  42564  fouriersw  42873  smflimlem1  43404  smflimlem6  43409  smfpimcc  43439  smfsuplem1  43442  smfinflem  43448  smflimsuplem1  43451  smflimsuplem2  43452  smflimsuplem3  43453  smflimsuplem4  43454  smflimsuplem5  43455  smflimsuplem7  43457  smfliminflem  43461  upwlksfval  44363