Theorem dmex 7616

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

Syntax hints:   ∈ wcel 2114  Vcvv 3494  dom cdm 5555

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 2793  ax-sep 5203  ax-nul 5210  ax-pr 5330  ax-un 7461

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 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-opab 5129  df-cnv 5563  df-dm 5565  df-rn 5566

This theorem is referenced by:  elxp4  7627  ofmres  7685  1stval  7691  fo1st  7709  frxp  7820  tfrlem8  8020  mapprc  8410  ixpprc  8483  bren  8518  brdomg  8519  fundmen  8583  domssex  8678  mapen  8681  ssenen  8691  hartogslem1  9006  brwdomn0  9033  unxpwdom2  9052  ixpiunwdom  9055  oemapwe  9157  cantnffval2  9158  r0weon  9438  fseqenlem2  9451  acndom  9477  acndom2  9480  dfac9  9562  ackbij2lem2  9662  ackbij2lem3  9663  cfsmolem  9692  coftr  9695  dcomex  9869  axdc3lem4  9875  axdclem  9941  axdclem2  9942  fodomb  9948  brdom3  9950  brdom5  9951  brdom4  9952  hashfacen  13813  shftfval  14429  prdsval  16728  isoval  17035  issubc  17105  prfval  17449  psgnghm2  20725  dfac14  22226  indishmph  22406  ufldom  22570  tsmsval2  22738  dvmptadd  24557  dvmptmul  24558  dvmptco  24569  taylfval  24947  usgrsizedg  26997  usgredgleordALT  27016  vtxdun  27263  vtxdlfgrval  27267  vtxd0nedgb  27270  vtxdushgrfvedglem  27271  vtxdushgrfvedg  27272  vtxdginducedm1lem4  27324  vtxdginducedm1  27325  ewlksfval  27383  wksfval  27391  wksv  27401  wlkiswwlksupgr2  27655  vdn0conngrumgrv2  27975  vdgn1frgrv2  28075  hmoval  28587  cyc3conja  30799  esum2d  31352  sitmval  31607  bnj893  32200  fmlafv  32627  fmla  32628  fmlasuc0  32631  dfrecs2  33411  dfrdg4  33412  indexdom  35024  dibfval  38292  aomclem1  39703  dfac21  39715  trclexi  40029  rtrclexi  40030  dfrtrcl5  40038  dfrcl2  40068  dvsubf  42247  dvdivf  42256  fouriersw  42565  smflimlem1  43096  smflimlem6  43101  smfpimcc  43131  smfsuplem1  43134  smfinflem  43140  smflimsuplem1  43143  smflimsuplem2  43144  smflimsuplem3  43145  smflimsuplem4  43146  smflimsuplem5  43147  smflimsuplem7  43149  smfliminflem  43153  upwlksfval  44059