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

Theorem dmexg 4927
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 4489 . 2  |-  ( A  e.  V  ->  U. A  e.  _V )
2 uniexg 4489 . 2  |-  ( U. A  e.  _V  ->  U.
U. A  e.  _V )
3 ssun1 3313 . . . 4  |-  dom  A  C_  ( dom  A  u.  ran  A )
4 dmrnssfld 4926 . . . 4  |-  ( dom 
A  u.  ran  A
)  C_  U. U. A
53, 4sstri 3163 . . 3  |-  dom  A  C_ 
U. U. A
6 ssexg 4134 . . 3  |-  ( ( dom  A  C_  U. U. A  /\  U. U. A  e.  _V )  ->  dom  A  e.  _V )
75, 6mpan 654 . 2  |-  ( U. U. A  e.  _V  ->  dom 
A  e.  _V )
81, 2, 73syl 20 1  |-  ( A  e.  V  ->  dom  A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 6    e. wcel 1621   _Vcvv 2763    u. cun 3125    C_ wss 3127   U.cuni 3801   dom cdm 4661   ran crn 4662
This theorem is referenced by:  dmex  4929  iprc  4931  exse2  5035  xpexr2  5103  soex  5110  cnvexg  5195  coexg  5202  dmfex  5362  cofunexg  5673  offval3  6025  tposexg  6182  tfrlem12  6373  tfrlem13  6374  erexb  6653  oion  7219  unxpwdom2  7270  wemapwe  7368  imadomg  8127  fpwwe2lem3  8223  fpwwe2lem12  8231  fpwwe2lem13  8232  hashfn  11324  o1of2  12052  prdsplusg  13321  prdsmulr  13322  prdsvsca  13323  prdshom  13329  ssclem  13659  ssc2  13662  ssctr  13665  subsubc  13690  resf1st  13731  resf2nd  13732  funcres  13733  spwex  14301  efgrcl  14987  dprdgrp  15203  dprdf  15204  dprdcntz  15206  dprddisj  15207  dprdw  15208  dprdssv  15214  dprdfid  15215  dprdfinv  15217  dprdfadd  15218  dprdfsub  15219  dprdfeq0  15220  dprdf11  15221  dprdlub  15224  dprdres  15226  dprdss  15227  dprdf1o  15230  subgdmdprd  15232  dmdprdsplitlem  15235  dprddisj2  15237  dprd2da  15240  dmdprdsplit2  15244  dpjfval  15253  dpjidcl  15256  ordtbaslem  16881  ordtuni  16883  ordtbas2  16884  ordtbas  16885  ordttopon  16886  ordtopn1  16887  ordtopn2  16888  ordtrest2lem  16896  ordtrest2  16897  txindislem  17290  ordthmeolem  17455  ptcmplem2  17710  mbfmulc2re  18966  mbfneg  18968  dvnff  19235  dchrptlem3  20468  ismgm  20948  iseupa  23254  bdayval  23672  axbday  23698  oprabex2gpop  24403  iscst1  24542  cur1val  24566  ppldrels  24595  sege  24620  supdef  24630  supdefa  24631  defge3  24639  inpc  24645  tailf  25692  tailfb  25694  f1lindf  26660  xpexcnv  27028
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239  ax-sep 4115  ax-nul 4123  ax-pr 4186  ax-un 4484
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2122  df-mo 2123  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-ne 2423  df-rex 2524  df-rab 2527  df-v 2765  df-dif 3130  df-un 3132  df-in 3134  df-ss 3141  df-nul 3431  df-if 3540  df-sn 3620  df-pr 3621  df-op 3623  df-uni 3802  df-br 3998  df-opab 4052  df-cnv 4677  df-dm 4679  df-rn 4680
  Copyright terms: Public domain W3C validator