Theorem dmex 7246

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

Syntax hints:   ∈ wcel 2145  Vcvv 3351  dom cdm 5249

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pr 5034  ax-un 7096

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-cnv 5257  df-dm 5259  df-rn 5260

This theorem is referenced by:  elxp4  7257  ofmres  7311  1stval  7317  fo1st  7335  frxp  7438  tfrlem8  7633  mapprc  8013  ixpprc  8083  bren  8118  brdomg  8119  ctex  8124  fundmen  8183  domssex  8277  mapen  8280  ssenen  8290  hartogslem1  8603  brwdomn0  8630  unxpwdom2  8649  ixpiunwdom  8652  oemapwe  8755  cantnffval2  8756  r0weon  9035  fseqenlem2  9048  acndom  9074  acndom2  9077  dfac9  9160  ackbij2lem2  9264  ackbij2lem3  9265  cfsmolem  9294  coftr  9297  dcomex  9471  axdc3lem4  9477  axdclem  9543  axdclem2  9544  fodomb  9550  brdom3  9552  brdom5  9553  brdom4  9554  hashfacen  13440  shftfval  14018  prdsval  16323  isoval  16632  issubc  16702  prfval  17047  symgbas  18007  psgnghm2  20142  dfac14  21642  indishmph  21822  ufldom  21986  tsmsval2  22153  dvmptadd  23943  dvmptmul  23944  dvmptco  23955  taylfval  24333  usgrsizedg  26329  usgredgleordALT  26349  vtxdun  26612  vtxdlfgrval  26616  vtxd0nedgb  26619  vtxdushgrfvedglem  26620  vtxdushgrfvedg  26621  vtxdginducedm1lem4  26673  vtxdginducedm1  26674  ewlksfval  26732  wksfval  26740  wksv  26750  wlkiswwlksupgr2  27011  vdn0conngrumgrv2  27376  vdgn1frgrv2  27478  hmoval  28005  esum2d  30495  sitmval  30751  bnj893  31336  dfrecs2  32394  dfrdg4  32395  cnfinltrel  33578  indexdom  33861  dibfval  36951  aomclem1  38150  dfac21  38162  trclexi  38453  rtrclexi  38454  dfrtrcl5  38462  dfrcl2  38492  dvsubf  40646  dvdivf  40655  fouriersw  40965  smflimlem1  41499  smflimlem6  41504  smfpimcc  41534  smfsuplem1  41537  smfinflem  41543  smflimsuplem1  41546  smflimsuplem2  41547  smflimsuplem3  41548  smflimsuplem4  41549  smflimsuplem5  41550  smflimsuplem7  41552  smfliminflem  41556  upwlksfval  42244