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

Theorem dmexg 4955
Description: The domain of a set is a set. Corollary 6.8(2) of [TakeutiZaring] p. 26. (Contributed by NM, 7-Apr-1995.)
Assertion
Ref Expression
dmexg  |-  ( A  e.  V  ->  dom  A  e.  _V )

Proof of Theorem dmexg
StepHypRef Expression
1 uniexg 4533 . 2  |-  ( A  e.  V  ->  U. A  e.  _V )
2 uniexg 4533 . 2  |-  ( U. A  e.  _V  ->  U.
U. A  e.  _V )
3 ssun1 3351 . . . 4  |-  dom  A  C_  ( dom  A  u.  ran  A )
4 dmrnssfld 4954 . . . 4  |-  ( dom 
A  u.  ran  A
)  C_  U. U. A
53, 4sstri 3201 . . 3  |-  dom  A  C_ 
U. U. A
6 ssexg 4176 . . 3  |-  ( ( dom  A  C_  U. U. A  /\  U. U. A  e.  _V )  ->  dom  A  e.  _V )
75, 6mpan 651 . 2  |-  ( U. U. A  e.  _V  ->  dom 
A  e.  _V )
81, 2, 73syl 18 1  |-  ( A  e.  V  ->  dom  A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696   _Vcvv 2801    u. cun 3163    C_ wss 3165   U.cuni 3843   dom cdm 4705   ran crn 4706
This theorem is referenced by:  dmex  4957  iprc  4959  exse2  5063  xpexr2  5131  soex  5138  cnvexg  5224  coexg  5231  dmfex  5440  cofunexg  5755  offval3  6107  tposexg  6264  tfrlem12  6421  tfrlem13  6422  erexb  6701  oion  7267  unxpwdom2  7318  wemapwe  7416  imadomg  8175  fpwwe2lem3  8271  fpwwe2lem12  8279  fpwwe2lem13  8280  hashfn  11373  o1of2  12102  prdsplusg  13374  prdsmulr  13375  prdsvsca  13376  prdshom  13382  ssclem  13712  ssc2  13715  ssctr  13718  subsubc  13743  resf1st  13784  resf2nd  13785  funcres  13786  spwex  14354  efgrcl  15040  dprdgrp  15256  dprdf  15257  dprdcntz  15259  dprddisj  15260  dprdw  15261  dprdssv  15267  dprdfid  15268  dprdfinv  15270  dprdfadd  15271  dprdfsub  15272  dprdfeq0  15273  dprdf11  15274  dprdlub  15277  dprdres  15279  dprdss  15280  dprdf1o  15283  subgdmdprd  15285  dmdprdsplitlem  15288  dprddisj2  15290  dprd2da  15293  dmdprdsplit2  15297  dpjfval  15306  dpjidcl  15309  ordtbaslem  16934  ordtuni  16936  ordtbas2  16937  ordtbas  16938  ordttopon  16939  ordtopn1  16940  ordtopn2  16941  ordtrest2lem  16949  ordtrest2  16950  txindislem  17343  ordthmeolem  17508  ptcmplem2  17763  mbfmulc2re  19019  mbfneg  19021  dvnff  19288  dchrptlem3  20521  ismgm  21003  ctex  23351  ofcfval3  23478  cndprobval  23651  iseupa  23896  bdayval  24373  bdayfo  24400  oprabex2gpop  25139  iscst1  25277  cur1val  25301  ppldrels  25330  sege  25355  supdef  25365  supdefa  25366  defge3  25374  inpc  25380  tailf  26427  tailfb  26429  f1lindf  27395  xpexcnv  27762  wlks  28328  wlkres  28331  trls  28335  crcts  28367  cycls  28368
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pr 4230  ax-un 4528
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-opab 4094  df-cnv 4713  df-dm 4715  df-rn 4716
  Copyright terms: Public domain W3C validator