Theorem dmex 7848

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

Syntax hints:   ∈ wcel 2113  Vcvv 3437  dom cdm 5621

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7677

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-cnv 5629  df-dm 5631  df-rn 5632

This theorem is referenced by:  elxp4  7861  ofmres  7925  1stval  7932  fo1st  7950  frxp  8065  frxp2  8083  frxp3  8090  tfrlem8  8312  mapprc  8763  ixpprc  8853  bren  8889  brdomg  8891  fundmen  8964  domssex  9062  mapen  9065  ssenen  9075  hartogslem1  9439  wemapso  9448  brwdomn0  9466  unxpwdom2  9485  ixpiunwdom  9487  oemapwe  9595  cantnffval2  9596  r0weon  9914  fseqenlem2  9927  acndom  9953  acndom2  9956  dfac9  10039  ackbij2lem2  10141  ackbij2lem3  10142  cfsmolem  10172  coftr  10175  dcomex  10349  axdc3lem4  10355  axdclem  10421  axdclem2  10422  fodomb  10428  brdom3  10430  brdom5  10431  brdom4  10432  shftfval  14984  prdsvallem  17365  isoval  17680  issubc  17750  prfval  18113  psgnghm2  21527  psdmul  22100  dfac14  23553  indishmph  23733  ufldom  23897  tsmsval2  24065  dvmptadd  25911  dvmptmul  25912  dvmptco  25923  taylfval  26313  usgrsizedg  29214  usgredgleordALT  29233  vtxdun  29481  vtxdlfgrval  29485  vtxd0nedgb  29488  vtxdushgrfvedglem  29489  vtxdushgrfvedg  29490  vtxdginducedm1lem4  29542  vtxdginducedm1  29543  ewlksfval  29601  wksfval  29609  wlkiswwlksupgr2  29876  vdn0conngrumgrv2  30197  vdgn1frgrv2  30297  hmoval  30811  cyc3conja  33167  esum2d  34178  sitmval  34434  bnj893  35012  fmlafv  35496  fmla  35497  fmlasuc0  35500  dfrecs2  36066  dfrdg4  36067  indexdom  37847  dibfval  41313  aomclem1  43211  dfac21  43223  trclexi  43777  rtrclexi  43778  dfrtrcl5  43786  dfrcl2  43831  dvsubf  46074  dvdivf  46082  fouriersw  46391  smflimlem1  46931  smflimlem6  46936  smfpimcc  46968  smfsuplem1  46971  smfinflem  46977  smflimsuplem1  46980  smflimsuplem2  46981  smflimsuplem3  46982  smflimsuplem4  46983  smflimsuplem5  46984  smflimsuplem7  46986  smfliminflem  46990  fsupdm  47002  finfdm  47006  grimidvtxedg  48047  isuspgrim0  48056  cycldlenngric  48090  upwlksfval  48297  dfinito4  49662  dftermo4  49663