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

Theorem dmex 5065
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 5063 . 2  |-  ( A  e.  _V  ->  dom  A  e.  _V )
31, 2ax-mp 8 1  |-  dom  A  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1717   _Vcvv 2892   dom cdm 4811
This theorem is referenced by:  elxp4  5290  ofmres  6275  1stval  6283  fo1st  6298  frxp  6385  tfrlem8  6574  mapprc  6951  ixpprc  7012  bren  7046  brdomg  7047  fundmen  7109  domssex  7197  mapen  7200  ssenen  7210  hartogslem1  7437  brwdomn0  7463  unxpwdom2  7482  ixpiunwdom  7485  oemapwe  7576  cantnffval2  7577  r0weon  7820  fseqenlem2  7832  acndom  7858  acndom2  7861  dfac9  7942  ackbij2lem2  8046  ackbij2lem3  8047  cfsmolem  8076  coftr  8079  dcomex  8253  axdc3lem4  8259  axdclem  8325  axdclem2  8326  fodomb  8330  brdom3  8332  brdom5  8333  brdom4  8334  hashfacen  11623  shftfval  11805  prdsval  13598  isoval  13910  issubc  13955  prfval  14216  symgbas  15015  dfac14  17564  indishmph  17744  ufldom  17908  tsmsval2  18073  dvmptadd  19706  dvmptmul  19707  dvmptco  19718  taylfval  20135  hmoval  22152  ctex  23934  dfrdg4  25506  tfrqfree  25507  indexdom  26120  aomclem1  26813  dfac21  26826  psgnghm2  27100  bnj893  28630  dibfval  31307
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361  ax-sep 4264  ax-nul 4272  ax-pr 4337  ax-un 4634
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2235  df-mo 2236  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-ne 2545  df-rex 2648  df-rab 2651  df-v 2894  df-dif 3259  df-un 3261  df-in 3263  df-ss 3270  df-nul 3565  df-if 3676  df-sn 3756  df-pr 3757  df-op 3759  df-uni 3951  df-br 4147  df-opab 4201  df-cnv 4819  df-dm 4821  df-rn 4822
  Copyright terms: Public domain W3C validator