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

Theorem dmex 6964
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 6962 . 2 (𝐴 ∈ V → dom 𝐴 ∈ V)
31, 2ax-mp 5 1 dom 𝐴 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 1975  Vcvv 3168  dom cdm 5024
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-8 1977  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-sep 4699  ax-nul 4708  ax-pr 4824  ax-un 6820
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2457  df-mo 2458  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-rex 2897  df-rab 2900  df-v 3170  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-if 4032  df-sn 4121  df-pr 4123  df-op 4127  df-uni 4363  df-br 4574  df-opab 4634  df-cnv 5032  df-dm 5034  df-rn 5035
This theorem is referenced by:  elxp4  6976  ofmres  7028  1stval  7034  fo1st  7052  frxp  7147  tfrlem8  7340  mapprc  7721  ixpprc  7788  bren  7823  brdomg  7824  ctex  7829  fundmen  7889  domssex  7979  mapen  7982  ssenen  7992  hartogslem1  8303  brwdomn0  8330  unxpwdom2  8349  ixpiunwdom  8352  oemapwe  8447  cantnffval2  8448  r0weon  8691  fseqenlem2  8704  acndom  8730  acndom2  8733  dfac9  8814  ackbij2lem2  8918  ackbij2lem3  8919  cfsmolem  8948  coftr  8951  dcomex  9125  axdc3lem4  9131  axdclem  9197  axdclem2  9198  fodomb  9202  brdom3  9204  brdom5  9205  brdom4  9206  hashfacen  13043  shftfval  13600  prdsval  15880  isoval  16190  issubc  16260  prfval  16604  symgbas  17565  psgnghm2  19687  dfac14  21169  indishmph  21349  ufldom  21514  tsmsval2  21681  dvmptadd  23442  dvmptmul  23443  dvmptco  23454  taylfval  23830  hmoval  26851  esum2d  29284  sitmval  29540  bnj893  30054  dfrecs2  31029  dfrdg4  31030  indexdom  32498  dibfval  35247  aomclem1  36441  dfac21  36453  trclexi  36745  rtrclexi  36746  dfrtrcl5  36754  dfrcl2  36784  dvsubf  38602  dvdivf  38612  fouriersw  38924  smflimlem1  39457  smflimlem6  39462  usgrsizedg  40440  usgredgaleordALT  40459  vtxdun  40694  vtxdlfgrval  40698  vtxd0nedgb  40701  vtxdushgrfvedglem  40702  vtxdushgrfvedg  40703  ewlksfval  40801  1wlksfval  40809  wlksfval  40810  1wlksv  40822  1wlkiswwlksupgr2  41072  vdn0conngrumgrv2  41361  vdgn1frgrv2  41464
  Copyright terms: Public domain W3C validator