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

Theorem dmexg 4892
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 4454 . 2  |-  ( A  e.  V  ->  U. A  e.  _V )
2 uniexg 4454 . 2  |-  ( U. A  e.  _V  ->  U.
U. A  e.  _V )
3 ssun1 3280 . . . 4  |-  dom  A  C_  ( dom  A  u.  ran  A )
4 dmrnssfld 4891 . . . 4  |-  ( dom 
A  u.  ran  A
)  C_  U. U. A
53, 4sstri 3130 . . 3  |-  dom  A  C_ 
U. U. A
6 ssexg 4100 . . 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 2740    u. cun 3092    C_ wss 3094   U.cuni 3768   dom cdm 4626   ran crn 4627
This theorem is referenced by:  dmex  4894  iprc  4896  exse2  5000  xpexr2  5068  soex  5075  cnvexg  5160  coexg  5167  dmfex  5327  cofunexg  5638  offval3  5990  tposexg  6147  tfrlem12  6338  tfrlem13  6339  erexb  6618  oion  7184  unxpwdom2  7235  wemapwe  7333  imadomg  8092  fpwwe2lem3  8188  fpwwe2lem12  8196  fpwwe2lem13  8197  hashfn  11288  o1of2  12016  prdsplusg  13285  prdsmulr  13286  prdsvsca  13287  prdshom  13293  ssclem  13623  ssc2  13626  ssctr  13629  subsubc  13654  resf1st  13695  resf2nd  13696  funcres  13697  spwex  14265  efgrcl  14951  dprdgrp  15167  dprdf  15168  dprdcntz  15170  dprddisj  15171  dprdw  15172  dprdssv  15178  dprdfid  15179  dprdfinv  15181  dprdfadd  15182  dprdfsub  15183  dprdfeq0  15184  dprdf11  15185  dprdlub  15188  dprdres  15190  dprdss  15191  dprdf1o  15194  subgdmdprd  15196  dmdprdsplitlem  15199  dprddisj2  15201  dprd2da  15204  dmdprdsplit2  15208  dpjfval  15217  dpjidcl  15220  ordtbaslem  16845  ordtuni  16847  ordtbas2  16848  ordtbas  16849  ordttopon  16850  ordtopn1  16851  ordtopn2  16852  ordtrest2lem  16860  ordtrest2  16861  txindislem  17254  ordthmeolem  17419  ptcmplem2  17674  mbfmulc2re  18930  mbfneg  18932  dvnff  19199  dchrptlem3  20432  ismgm  20912  iseupa  23218  bdayval  23636  axbday  23662  oprabex2gpop  24367  iscst1  24506  cur1val  24530  ppldrels  24559  sege  24584  supdef  24594  supdefa  24595  defge3  24603  inpc  24609  tailf  25656  tailfb  25658  f1lindf  26624  xpexcnv  26992
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 2237  ax-sep 4081  ax-nul 4089  ax-pr 4152  ax-un 4449
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 2121  df-mo 2122  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-rex 2521  df-rab 2523  df-v 2742  df-dif 3097  df-un 3099  df-in 3101  df-ss 3108  df-nul 3398  df-if 3507  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3769  df-br 3964  df-opab 4018  df-cnv 4642  df-dm 4644  df-rn 4645
  Copyright terms: Public domain W3C validator