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

Theorem dmex 5132
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 5130 . 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 1725   _Vcvv 2956   dom cdm 4878
This theorem is referenced by:  elxp4  5357  ofmres  6343  1stval  6351  fo1st  6366  frxp  6456  tfrlem8  6645  mapprc  7022  ixpprc  7083  bren  7117  brdomg  7118  fundmen  7180  domssex  7268  mapen  7271  ssenen  7281  hartogslem1  7511  brwdomn0  7537  unxpwdom2  7556  ixpiunwdom  7559  oemapwe  7650  cantnffval2  7651  r0weon  7894  fseqenlem2  7906  acndom  7932  acndom2  7935  dfac9  8016  ackbij2lem2  8120  ackbij2lem3  8121  cfsmolem  8150  coftr  8153  dcomex  8327  axdc3lem4  8333  axdclem  8399  axdclem2  8400  fodomb  8404  brdom3  8406  brdom5  8407  brdom4  8408  hashfacen  11703  shftfval  11885  prdsval  13678  isoval  13990  issubc  14035  prfval  14296  symgbas  15095  dfac14  17650  indishmph  17830  ufldom  17994  tsmsval2  18159  dvmptadd  19846  dvmptmul  19847  dvmptco  19858  taylfval  20275  hmoval  22311  ctex  24100  sitmval  24661  dfrdg4  25795  tfrqfree  25796  indexdom  26436  aomclem1  27129  dfac21  27141  psgnghm2  27415  bnj893  29299  dibfval  31939
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-sep 4330  ax-nul 4338  ax-pr 4403  ax-un 4701
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-rex 2711  df-rab 2714  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-if 3740  df-sn 3820  df-pr 3821  df-op 3823  df-uni 4016  df-br 4213  df-opab 4267  df-cnv 4886  df-dm 4888  df-rn 4889
  Copyright terms: Public domain W3C validator