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

Theorem dmex 6745
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 6743 . 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 1904   _Vcvv 3031   dom cdm 4839
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pr 4639  ax-un 6602
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-rex 2762  df-rab 2765  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966  df-uni 4191  df-br 4396  df-opab 4455  df-cnv 4847  df-dm 4849  df-rn 4850
This theorem is referenced by:  elxp4  6756  ofmres  6808  1stval  6814  fo1st  6832  frxp  6925  tfrlem8  7120  mapprc  7494  ixpprc  7561  bren  7596  brdomg  7597  ctex  7602  fundmen  7661  domssex  7751  mapen  7754  ssenen  7764  hartogslem1  8075  brwdomn0  8102  unxpwdom2  8121  ixpiunwdom  8124  oemapwe  8217  cantnffval2  8218  r0weon  8461  fseqenlem2  8474  acndom  8500  acndom2  8503  dfac9  8584  ackbij2lem2  8688  ackbij2lem3  8689  cfsmolem  8718  coftr  8721  dcomex  8895  axdc3lem4  8901  axdclem  8967  axdclem2  8968  fodomb  8972  brdom3  8974  brdom5  8975  brdom4  8976  hashfacen  12658  shftfval  13210  prdsval  15431  isoval  15748  issubc  15818  prfval  16162  symgbas  17099  psgnghm2  19226  dfac14  20710  indishmph  20890  ufldom  21055  tsmsval2  21222  dvmptadd  22993  dvmptmul  22994  dvmptco  23005  taylfval  23393  hmoval  26532  esum2d  28988  sitmval  29255  bnj893  29811  dfrecs2  30788  dfrdg4  30789  indexdom  32125  dibfval  34780  aomclem1  35983  dfac21  35995  trclexi  36298  rtrclexi  36299  dfrtrcl5  36307  dfrcl2  36337  dvsubf  37881  dvdivf  37891  fouriersw  38207  usgredgaleordALT  39475  vtxdun  39704  vtxdlfgrval  39708  vtxd0nedgb  39711  vtxdushgrfvedglem  39712  vtxdushgrfvedg  39713  ewlksfval  39807  1wlksfval  39813  wlksfval  39814  1wlksv  39823  usgsizedg  40215  usgsizedgALT  40216  usgsizedgALT2  40217
  Copyright terms: Public domain W3C validator