MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dmex Structured version   Visualization version   GIF version

Theorem dmex 7096
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
StepHypRef Expression
1 dmex.1 . 2 𝐴 ∈ V
2 dmexg 7094 . 2 (𝐴 ∈ V → dom 𝐴 ∈ V)
31, 2ax-mp 5 1 dom 𝐴 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 1989  Vcvv 3198  dom cdm 5112
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1721  ax-4 1736  ax-5 1838  ax-6 1887  ax-7 1934  ax-8 1991  ax-9 1998  ax-10 2018  ax-11 2033  ax-12 2046  ax-13 2245  ax-ext 2601  ax-sep 4779  ax-nul 4787  ax-pr 4904  ax-un 6946
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1485  df-ex 1704  df-nf 1709  df-sb 1880  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2752  df-rex 2917  df-rab 2920  df-v 3200  df-dif 3575  df-un 3577  df-in 3579  df-ss 3586  df-nul 3914  df-if 4085  df-sn 4176  df-pr 4178  df-op 4182  df-uni 4435  df-br 4652  df-opab 4711  df-cnv 5120  df-dm 5122  df-rn 5123
This theorem is referenced by:  elxp4  7107  ofmres  7161  1stval  7167  fo1st  7185  frxp  7284  tfrlem8  7477  mapprc  7858  ixpprc  7926  bren  7961  brdomg  7962  ctex  7967  fundmen  8027  domssex  8118  mapen  8121  ssenen  8131  hartogslem1  8444  brwdomn0  8471  unxpwdom2  8490  ixpiunwdom  8493  oemapwe  8588  cantnffval2  8589  r0weon  8832  fseqenlem2  8845  acndom  8871  acndom2  8874  dfac9  8955  ackbij2lem2  9059  ackbij2lem3  9060  cfsmolem  9089  coftr  9092  dcomex  9266  axdc3lem4  9272  axdclem  9338  axdclem2  9339  fodomb  9345  brdom3  9347  brdom5  9348  brdom4  9349  hashfacen  13233  shftfval  13804  prdsval  16109  isoval  16419  issubc  16489  prfval  16833  symgbas  17794  psgnghm2  19921  dfac14  21415  indishmph  21595  ufldom  21760  tsmsval2  21927  dvmptadd  23717  dvmptmul  23718  dvmptco  23729  taylfval  24107  usgrsizedg  26101  usgredgleordALT  26120  vtxdun  26371  vtxdlfgrval  26375  vtxd0nedgb  26378  vtxdushgrfvedglem  26379  vtxdushgrfvedg  26380  vtxdginducedm1lem4  26432  vtxdginducedm1  26433  ewlksfval  26491  wksfval  26499  wksv  26509  wlkiswwlksupgr2  26757  vdn0conngrumgrv2  27049  vdgn1frgrv2  27153  hmoval  27649  esum2d  30140  sitmval  30396  bnj893  30983  dfrecs2  32041  dfrdg4  32042  indexdom  33509  dibfval  36256  aomclem1  37450  dfac21  37462  trclexi  37753  rtrclexi  37754  dfrtrcl5  37762  dfrcl2  37792  dvsubf  39897  dvdivf  39906  fouriersw  40217  smflimlem1  40748  smflimlem6  40753  smfpimcc  40783  smfsuplem1  40786  smfinflem  40792  smflimsuplem1  40795  smflimsuplem2  40796  smflimsuplem3  40797  smflimsuplem4  40798  smflimsuplem5  40799  smflimsuplem7  40801  smfliminflem  40805  upwlksfval  41487
  Copyright terms: Public domain W3C validator