Theorem dmexg 6751

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 6615	. 2 |- ( A e. V -> U. A e. _V )
2		uniexg 6615	. 2 |- ( U. A e. _V -> U. U. A e. _V )
3		ssun1 3609	. . . 4 |- dom A C_ ( dom A u. ran A )
4		dmrnssfld 5112	. . . 4 |- ( dom A u. ran A ) C_ U. U. A
5	3, 4	sstri 3453	. . 3 |- dom A C_ U. U. A
6		ssexg 4563	. . 3 |- ( ( dom A C_ U. U. A /\ U. U. A e. _V ) -> dom A e. _V )
7	5, 6	mpan 681	. 2 |- ( U. U. A e. _V -> dom A e. _V )
8	1, 2, 7	3syl 18	1 |- ( A e. V -> dom A e. _V )

Syntax hints:   -> wi 4   e. wcel 1898   _Vcvv 3057   u. cun 3414   C_ wss 3416   U.cuni 4212   dom cdm 4853   ran crn 4854

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pr 4653  ax-un 6610

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-rex 2755  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-uni 4213  df-br 4417  df-opab 4476  df-cnv 4861  df-dm 4863  df-rn 4864

This theorem is referenced by:  dmex  6753  iprc  6755  exse2  6759  xpexr2  6761  xpexcnv  6762  soex  6763  cnvexg  6766  coexg  6771  dmfex  6778  cofunexg  6784  offval3  6814  suppval  6943  funsssuppss  6968  suppss  6972  suppssov1  6974  suppssfv  6978  tposexg  7013  tfrlem12  7133  tfrlem13  7134  erexb  7414  f1vrnfibi  7885  oion  8077  unxpwdom2  8129  wemapwe  8228  imadomg  8988  fpwwe2lem3  9084  fpwwe2lem12  9092  fpwwe2lem13  9093  hashfn  12586  hashimarn  12643  trclexlem  13107  relexp0g  13134  relexpsucnnr  13137  o1of2  13725  prdsplusg  15405  prdsmulr  15406  prdsvsca  15407  prdshom  15414  isofn  15729  ssclem  15773  ssc2  15776  ssctr  15779  subsubc  15807  resf1st  15848  resf2nd  15849  funcres  15850  efgrcl  17414  dprddomprc  17681  dprdval0prc  17683  dprdgrp  17686  dprdf  17687  dprdssv  17698  subgdmdprd  17716  dprd2da  17724  f1lindf  19429  decpmatval0  19837  pmatcollpw3lem  19856  ordtbaslem  20253  ordtuni  20255  ordtbas2  20256  ordtbas  20257  ordttopon  20258  ordtopn1  20259  ordtopn2  20260  ordtrest2lem  20268  ordtrest2  20269  txindislem  20697  ordthmeolem  20865  ptcmplem2  21117  tuslem  21331  mbfmulc2re  22653  mbfneg  22655  dvnff  22926  dchrptlem3  24243  fiusgraedgfi  25184  sizeusglecusg  25263  wlks  25296  wlkres  25299  trls  25315  crcts  25399  cycls  25400  vdusgraval  25684  vdgrnn0pnf  25686  hashnbgravdg  25690  usgravd0nedg  25695  iseupa  25742  vdgn0frgrav2  25801  vdgn1frgrav2  25803  vdgfrgragt2  25804  ismgmOLD  26097  gsummpt2d  28593  ofcfval3  28972  braew  29114  omsval  29166  omsvalOLD  29170  sibfof  29222  sitmcl  29233  cndprobval  29315  bdayval  30584  bdayfo  30613  tailf  31080  tailfb  31082  rclexi  36267  rtrclexlem  36268  trclubgNEW  36270  cnvrcl0  36277  dfrtrcl5  36281  relexpmulg  36347  relexp01min  36350  relexpxpmin  36354  unidmex  37426  caragenval  38352  omecl  38362  caragenunidm  38367  opabn1stprc  39047  fundmge2nop  39068  fun2dmnop  39069  structgrssvtxlem  39171  vtxdgf  39581  offval0  40576