Theorem dmex 7922

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

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450  dom cdm 5650

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390  ax-un 7752

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-cnv 5658  df-dm 5660  df-rn 5661

This theorem is used by:  elxp4  7935  ofmres  7997  1stval  8004  fo1st  8022  frxp  8141  frxp2  8164  frxp3  8171  tfrlem8  8396  mapprc  8855  ixpprc  8951  bren  8987  brdomg  8989  fundmen  9063  domssex  9161  mapen  9164  ssenen  9174  hartogslem1  9540  wemapso  9549  brwdomn0  9567  unxpwdom2  9586  ixpiunwdom  9588  oemapwe  9699  cantnffval2  9700  r0weon  10095  fseqenlem2  10108  acndom  10134  acndom2  10137  dfac9  10219  ackbij2lem2  10321  ackbij2lem3  10322  cfsmolem  10352  coftr  10355  dcomex  10529  axdc3lem4  10535  axdclem  10601  axdclem2  10602  fodomb  10609  brdom3  10611  brdom5  10612  brdom4  10613  shftfval  15229  prdsvallem  17631  isoval  17946  issubc  18016  prfval  18379  psgnghm2  21893  psdmul  22493  dfac14  23943  indishmph  24123  ufldom  24287  tsmsval2  24455  dvmptadd  26286  dvmptmul  26287  dvmptco  26298  taylfval  26692  usgrsizedg  29802  usgredgleordALT  29821  vtxdun  30068  vtxdlfgrval  30072  vtxd0nedgb  30075  vtxdushgrfvedglem  30076  vtxdushgrfvedg  30077  vtxdginducedm1lem4  30129  vtxdginducedm1  30130  ewlksfval  30188  wksfval  30196  wlkiswwlksupgr2  30472  vdn0conngrumgrv2  30803  vdgn1frgrv2  30903  hmoval  31418  cyc3conja  33765  esum2d  34772  sitmval  35028  bnj893  35605  fmlafv  36232  fmla  36233  fmlasuc0  36236  dfrecs2  36807  dfrdg4  36808  indexdom  38762  dibfval  42292  aomclem1  44150  dfac21  44162  trclexi  44714  rtrclexi  44715  dfrtrcl5  44723  dfrcl2  44768  dvsubf  47018  dvdivf  47026  fouriersw  47335  smflimlem1  47875  smflimlem6  47880  smfpimcc  47912  smfsuplem1  47915  smfinflem  47921  smflimsuplem1  47924  smflimsuplem2  47925  smflimsuplem3  47926  smflimsuplem4  47927  smflimsuplem5  47928  smflimsuplem7  47930  smfliminflem  47934  fsupdm  47946  finfdm  47950  grimidvtxedg  49077  isuspgrim0  49086  cycldlenngric  49120  upwlksfval  49327  dfinito4  50730  dftermo4  50731