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

Theorem dmexg 4846
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 4408 . 2  |-  ( A  e.  V  ->  U. A  e.  _V )
2 uniexg 4408 . 2  |-  ( U. A  e.  _V  ->  U.
U. A  e.  _V )
3 ssun1 3248 . . . 4  |-  dom  A  C_  ( dom  A  u.  ran  A )
4 dmrnssfld 4845 . . . 4  |-  ( dom 
A  u.  ran  A
)  C_  U. U. A
53, 4sstri 3109 . . 3  |-  dom  A  C_ 
U. U. A
6 ssexg 4057 . . 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 2727    u. cun 3076    C_ wss 3078   U.cuni 3727   dom cdm 4580   ran crn 4581
This theorem is referenced by:  dmex  4848  iprc  4850  exse2  4954  xpexr2  5022  soex  5029  cnvexg  5114  coexg  5121  dmfex  5281  cofunexg  5591  offval3  5943  tposexg  6100  tfrlem12  6291  tfrlem13  6292  erexb  6571  oion  7135  unxpwdom2  7186  wemapwe  7284  imadomg  8043  fpwwe2lem3  8135  fpwwe2lem12  8143  fpwwe2lem13  8144  hashfn  11235  o1of2  11963  prdsplusg  13232  prdsmulr  13233  prdsvsca  13234  prdshom  13240  ssclem  13540  ssc2  13543  ssctr  13546  subsubc  13571  resf1st  13612  resf2nd  13613  funcres  13614  spwex  14173  efgrcl  14859  dprdgrp  15075  dprdf  15076  dprdcntz  15078  dprddisj  15079  dprdw  15080  dprdssv  15086  dprdfid  15087  dprdfinv  15089  dprdfadd  15090  dprdfsub  15091  dprdfeq0  15092  dprdf11  15093  dprdlub  15096  dprdres  15098  dprdss  15099  dprdf1o  15102  subgdmdprd  15104  dmdprdsplitlem  15107  dprddisj2  15109  dprd2da  15112  dmdprdsplit2  15116  dpjfval  15125  dpjidcl  15128  ordtbaslem  16750  ordtuni  16752  ordtbas2  16753  ordtbas  16754  ordttopon  16755  ordtopn1  16756  ordtopn2  16757  ordtrest2lem  16765  ordtrest2  16766  txindislem  17159  ordthmeolem  17324  ptcmplem2  17579  mbfmulc2re  18835  mbfneg  18837  dvnff  19104  dchrptlem3  20337  ismgm  20817  iseupa  23052  bdayval  23470  axbday  23496  oprabex2gpop  24201  iscst1  24340  cur1val  24364  ppldrels  24393  sege  24418  supdef  24428  supdefa  24429  defge3  24437  inpc  24443  tailf  25490  tailfb  25492  f1lindf  26458  xpexcnv  26826
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 1926  ax-ext 2234  ax-sep 4038  ax-nul 4046  ax-pr 4108  ax-un 4403
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 1883  df-eu 2118  df-mo 2119  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-rex 2514  df-rab 2516  df-v 2729  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-nul 3363  df-if 3471  df-sn 3550  df-pr 3551  df-op 3553  df-uni 3728  df-br 3921  df-opab 3975  df-cnv 4596  df-dm 4598  df-rn 4599
  Copyright terms: Public domain W3C validator