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

Theorem dmex 6731
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 6729 . 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 1889   _Vcvv 3047   dom cdm 4837
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pr 4642  ax-un 6588
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-eu 2305  df-mo 2306  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-rex 2745  df-rab 2748  df-v 3049  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-sn 3971  df-pr 3973  df-op 3977  df-uni 4202  df-br 4406  df-opab 4465  df-cnv 4845  df-dm 4847  df-rn 4848
This theorem is referenced by:  elxp4  6742  ofmres  6794  1stval  6800  fo1st  6818  frxp  6911  tfrlem8  7107  mapprc  7481  ixpprc  7548  bren  7583  brdomg  7584  ctex  7589  fundmen  7648  domssex  7738  mapen  7741  ssenen  7751  hartogslem1  8062  brwdomn0  8089  unxpwdom2  8108  ixpiunwdom  8111  oemapwe  8204  cantnffval2  8205  r0weon  8448  fseqenlem2  8461  acndom  8487  acndom2  8490  dfac9  8571  ackbij2lem2  8675  ackbij2lem3  8676  cfsmolem  8705  coftr  8708  dcomex  8882  axdc3lem4  8888  axdclem  8954  axdclem2  8955  fodomb  8959  brdom3  8961  brdom5  8962  brdom4  8963  hashfacen  12624  shftfval  13145  prdsval  15365  isoval  15682  issubc  15752  prfval  16096  symgbas  17033  psgnghm2  19161  dfac14  20645  indishmph  20825  ufldom  20989  tsmsval2  21156  dvmptadd  22926  dvmptmul  22927  dvmptco  22938  taylfval  23326  hmoval  26463  esum2d  28926  sitmval  29194  bnj893  29751  dfrecs2  30729  dfrdg4  30730  indexdom  32073  dibfval  34721  aomclem1  35924  dfac21  35936  trclexi  36239  rtrclexi  36240  dfrtrcl5  36248  dfrcl2  36278  dvsubf  37794  dvdivf  37804  fouriersw  38105  usgredgaleordALT  39321  vtxduhgrun  39548  vtxdumgrval  39550  vtxdushgrfvedglem  39552  vtxdushgrfvedg  39553  uhgrvd0nedgb  39555  ewlksfval  39628  1wlksfval  39634  wlksfval  39635  1wlksv  39642  usgsizedg  39811  usgsizedgALT  39812  usgsizedgALT2  39813
  Copyright terms: Public domain W3C validator