Theorem dmexg 6630

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

Step	Hyp	Ref	Expression
1		uniexg 6496	. 2 |- ( A e. V -> U. A e. _V )
2		uniexg 6496	. 2 |- ( U. A e. _V -> U. U. A e. _V )
3		ssun1 3581	. . . 4 |- dom A C_ ( dom A u. ran A )
4		dmrnssfld 5174	. . . 4 |- ( dom A u. ran A ) C_ U. U. A
5	3, 4	sstri 3426	. . 3 |- dom A C_ U. U. A
6		ssexg 4511	. . 3 |- ( ( dom A C_ U. U. A /\ U. U. A e. _V ) -> dom A e. _V )
7	5, 6	mpan 668	. 2 |- ( U. U. A e. _V -> dom A e. _V )
8	1, 2, 7	3syl 20	1 |- ( A e. V -> dom A e. _V )

Syntax hints:   -> wi 4   e. wcel 1826   _Vcvv 3034   u. cun 3387   C_ wss 3389   U.cuni 4163   dom cdm 4913   ran crn 4914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pr 4601  ax-un 6491

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-rex 2738  df-rab 2741  df-v 3036  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-br 4368  df-opab 4426  df-cnv 4921  df-dm 4923  df-rn 4924

This theorem is referenced by:  dmex  6632  iprc  6634  exse2  6638  xpexr2  6640  xpexcnv  6641  soex  6642  cnvexg  6645  coexg  6650  dmfex  6657  cofunexg  6663  offval3  6693  suppval  6819  funsssuppss  6844  suppss  6848  suppssov1  6850  suppssfv  6854  tposexg  6887  tfrlem12  6976  tfrlem13  6977  erexb  7254  oion  7876  unxpwdom2  7929  wemapwe  8052  wemapweOLD  8053  imadomg  8825  fpwwe2lem3  8922  fpwwe2lem12  8930  fpwwe2lem13  8931  hashfn  12346  hashimarn  12400  trclexlem  12832  relexp0g  12859  relexpsucnnr  12862  o1of2  13437  prdsplusg  14865  prdsmulr  14866  prdsvsca  14867  prdshom  14874  isofn  15181  ssclem  15225  ssc2  15228  ssctr  15231  subsubc  15259  resf1st  15300  resf2nd  15301  funcres  15302  efgrcl  16850  dprddomprc  17144  dprdval0prc  17146  dprdgrp  17151  dprdf  17152  dprdwOLD  17163  dprdssv  17169  dprdfidOLD  17177  dprdfinvOLD  17179  dprdfaddOLD  17180  dprdfsubOLD  17181  dprdfeq0OLD  17182  dprdf11OLD  17183  subgdmdprd  17194  dmdprdsplitlemOLD  17198  dprddisj2OLD  17201  dprd2da  17204  dpjidclOLD  17227  f1lindf  18942  decpmatval0  19350  pmatcollpw3lem  19369  ordtbaslem  19775  ordtuni  19777  ordtbas2  19778  ordtbas  19779  ordttopon  19780  ordtopn1  19781  ordtopn2  19782  ordtrest2lem  19790  ordtrest2  19791  txindislem  20219  ordthmeolem  20387  ptcmplem2  20638  tuslem  20855  mbfmulc2re  22140  mbfneg  22142  dvnff  22411  dchrptlem3  23658  fiusgraedgfi  24528  sizeusglecusg  24607  wlks  24640  wlkres  24643  trls  24659  crcts  24743  cycls  24744  vdusgraval  25028  vdgrnn0pnf  25030  hashnbgravdg  25034  usgravd0nedg  25039  iseupa  25086  vdgn0frgrav2  25145  vdgn1frgrav2  25147  vdgfrgragt2  25148  ismgmOLD  25439  gsummpt2d  27925  ofcfval3  28250  braew  28370  omsval  28420  sibfof  28465  cndprobval  28555  bdayval  29573  bdayfo  29600  tailf  30359  tailfb  30361  f1vrnfibi  32634  offval0  33311  relexp01min  38237  relexpxpmin  38244  relexpmulg  38246