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

Theorem dmexg 4913
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 4475 . 2  |-  ( A  e.  V  ->  U. A  e.  _V )
2 uniexg 4475 . 2  |-  ( U. A  e.  _V  ->  U.
U. A  e.  _V )
3 ssun1 3299 . . . 4  |-  dom  A  C_  ( dom  A  u.  ran  A )
4 dmrnssfld 4912 . . . 4  |-  ( dom 
A  u.  ran  A
)  C_  U. U. A
53, 4sstri 3149 . . 3  |-  dom  A  C_ 
U. U. A
6 ssexg 4120 . . 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 2757    u. cun 3111    C_ wss 3113   U.cuni 3787   dom cdm 4647   ran crn 4648
This theorem is referenced by:  dmex  4915  iprc  4917  exse2  5021  xpexr2  5089  soex  5096  cnvexg  5181  coexg  5188  dmfex  5348  cofunexg  5659  offval3  6011  tposexg  6168  tfrlem12  6359  tfrlem13  6360  erexb  6639  oion  7205  unxpwdom2  7256  wemapwe  7354  imadomg  8113  fpwwe2lem3  8209  fpwwe2lem12  8217  fpwwe2lem13  8218  hashfn  11309  o1of2  12037  prdsplusg  13306  prdsmulr  13307  prdsvsca  13308  prdshom  13314  ssclem  13644  ssc2  13647  ssctr  13650  subsubc  13675  resf1st  13716  resf2nd  13717  funcres  13718  spwex  14286  efgrcl  14972  dprdgrp  15188  dprdf  15189  dprdcntz  15191  dprddisj  15192  dprdw  15193  dprdssv  15199  dprdfid  15200  dprdfinv  15202  dprdfadd  15203  dprdfsub  15204  dprdfeq0  15205  dprdf11  15206  dprdlub  15209  dprdres  15211  dprdss  15212  dprdf1o  15215  subgdmdprd  15217  dmdprdsplitlem  15220  dprddisj2  15222  dprd2da  15225  dmdprdsplit2  15229  dpjfval  15238  dpjidcl  15241  ordtbaslem  16866  ordtuni  16868  ordtbas2  16869  ordtbas  16870  ordttopon  16871  ordtopn1  16872  ordtopn2  16873  ordtrest2lem  16881  ordtrest2  16882  txindislem  17275  ordthmeolem  17440  ptcmplem2  17695  mbfmulc2re  18951  mbfneg  18953  dvnff  19220  dchrptlem3  20453  ismgm  20933  iseupa  23239  bdayval  23657  axbday  23683  oprabex2gpop  24388  iscst1  24527  cur1val  24551  ppldrels  24580  sege  24605  supdef  24615  supdefa  24616  defge3  24624  inpc  24630  tailf  25677  tailfb  25679  f1lindf  26645  xpexcnv  27013
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 4101  ax-nul 4109  ax-pr 4172  ax-un 4470
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 2522  df-rab 2525  df-v 2759  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-nul 3417  df-if 3526  df-sn 3606  df-pr 3607  df-op 3609  df-uni 3788  df-br 3984  df-opab 4038  df-cnv 4663  df-dm 4665  df-rn 4666
  Copyright terms: Public domain W3C validator