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

Theorem dmexg 5122
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 4698 . 2  |-  ( A  e.  V  ->  U. A  e.  _V )
2 uniexg 4698 . 2  |-  ( U. A  e.  _V  ->  U.
U. A  e.  _V )
3 ssun1 3502 . . . 4  |-  dom  A  C_  ( dom  A  u.  ran  A )
4 dmrnssfld 5121 . . . 4  |-  ( dom 
A  u.  ran  A
)  C_  U. U. A
53, 4sstri 3349 . . 3  |-  dom  A  C_ 
U. U. A
6 ssexg 4341 . . 3  |-  ( ( dom  A  C_  U. U. A  /\  U. U. A  e.  _V )  ->  dom  A  e.  _V )
75, 6mpan 652 . 2  |-  ( U. U. A  e.  _V  ->  dom 
A  e.  _V )
81, 2, 73syl 19 1  |-  ( A  e.  V  ->  dom  A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725   _Vcvv 2948    u. cun 3310    C_ wss 3312   U.cuni 4007   dom cdm 4870   ran crn 4871
This theorem is referenced by:  dmex  5124  iprc  5126  exse2  5230  xpexr2  5300  soex  5311  cnvexg  5397  coexg  5404  dmfex  5618  cofunexg  5951  offval3  6310  tposexg  6485  tfrlem12  6642  tfrlem13  6643  erexb  6922  oion  7497  unxpwdom2  7548  wemapwe  7646  imadomg  8404  fpwwe2lem3  8500  fpwwe2lem12  8508  fpwwe2lem13  8509  hashfn  11641  o1of2  12398  prdsplusg  13673  prdsmulr  13674  prdsvsca  13675  prdshom  13681  ssclem  14011  ssc2  14014  ssctr  14017  subsubc  14042  resf1st  14083  resf2nd  14084  funcres  14085  spwex  14653  efgrcl  15339  dprdgrp  15555  dprdf  15556  dprdcntz  15558  dprddisj  15559  dprdw  15560  dprdssv  15566  dprdfid  15567  dprdfinv  15569  dprdfadd  15570  dprdfsub  15571  dprdfeq0  15572  dprdf11  15573  dprdlub  15576  dprdres  15578  dprdss  15579  dprdf1o  15582  subgdmdprd  15584  dmdprdsplitlem  15587  dprddisj2  15589  dprd2da  15592  dmdprdsplit2  15596  dpjfval  15605  dpjidcl  15608  ordtbaslem  17244  ordtuni  17246  ordtbas2  17247  ordtbas  17248  ordttopon  17249  ordtopn1  17250  ordtopn2  17251  ordtrest2lem  17259  ordtrest2  17260  txindislem  17657  ordthmeolem  17825  ptcmplem2  18076  tuslem  18289  mbfmulc2re  19532  mbfneg  19534  dvnff  19801  dchrptlem3  21042  fiusgraedgfi  21413  sizeusglecusg  21487  wlks  21518  wlkres  21521  trls  21528  crcts  21601  cycls  21602  vdusgraval  21670  vdgrnn0pnf  21672  hashnbgravdg  21674  usgravd0nedg  21675  iseupa  21679  ismgm  21900  ofcfval3  24477  braew  24585  sibfof  24646  sitmcl  24655  cndprobval  24683  bdayval  25595  bdayfo  25622  tailf  26395  tailfb  26397  f1lindf  27260  xpexcnv  27626  hashimarn  28141  vdgn0frgrav2  28352  vdgn1frgrav2  28354  vdgfrgragt2  28355
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pr 4395  ax-un 4693
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-rex 2703  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-opab 4259  df-cnv 4878  df-dm 4880  df-rn 4881
  Copyright terms: Public domain W3C validator