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

Theorem dmex 6739
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  |-  A  e. 
_V
Assertion
Ref Expression
dmex  |-  dom  A  e.  _V

Proof of Theorem dmex
StepHypRef Expression
1 dmex.1 . 2  |-  A  e. 
_V
2 dmexg 6737 . 2  |-  ( A  e.  _V  ->  dom  A  e.  _V )
31, 2ax-mp 5 1  |-  dom  A  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1869   _Vcvv 3082   dom cdm 4852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4545  ax-nul 4554  ax-pr 4659  ax-un 6596
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-rex 2782  df-rab 2785  df-v 3084  df-dif 3441  df-un 3443  df-in 3445  df-ss 3452  df-nul 3764  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4219  df-br 4423  df-opab 4482  df-cnv 4860  df-dm 4862  df-rn 4863
This theorem is referenced by:  elxp4  6750  ofmres  6802  1stval  6808  fo1st  6826  frxp  6916  tfrlem8  7112  mapprc  7486  ixpprc  7553  bren  7588  brdomg  7589  fundmen  7652  domssex  7741  mapen  7744  ssenen  7754  hartogslem1  8065  brwdomn0  8092  unxpwdom2  8111  ixpiunwdom  8114  oemapwe  8206  cantnffval2  8207  r0weon  8450  fseqenlem2  8462  acndom  8488  acndom2  8491  dfac9  8572  ackbij2lem2  8676  ackbij2lem3  8677  cfsmolem  8706  coftr  8709  dcomex  8883  axdc3lem4  8889  axdclem  8955  axdclem2  8956  fodomb  8960  brdom3  8962  brdom5  8963  brdom4  8964  hashfacen  12620  shftfval  13131  prdsval  15350  isoval  15667  issubc  15737  prfval  16081  symgbas  17018  psgnghm2  19145  dfac14  20629  indishmph  20809  ufldom  20973  tsmsval2  21140  dvmptadd  22910  dvmptmul  22911  dvmptco  22922  taylfval  23310  hmoval  26447  ctex  28296  esum2d  28920  sitmval  29188  bnj893  29745  dfrecs2  30720  dfrdg4  30721  indexdom  32023  dibfval  34676  aomclem1  35880  dfac21  35892  dfrcl2  36174  dvsubf  37652  dvdivf  37662  fouriersw  37963  usgredgaleord  38979  usgsizedg  39099  usgsizedgALT  39100  usgsizedgALT2  39101
  Copyright terms: Public domain W3C validator