Theorem dmexg 6705

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 6572	. 2 |- ( A e. V -> U. A e. _V )
2		uniexg 6572	. 2 |- ( U. A e. _V -> U. U. A e. _V )
3		ssun1 3660	. . . 4 |- dom A C_ ( dom A u. ran A )
4		dmrnssfld 5252	. . . 4 |- ( dom A u. ran A ) C_ U. U. A
5	3, 4	sstri 3506	. . 3 |- dom A C_ U. U. A
6		ssexg 4586	. . 3 |- ( ( dom A C_ U. U. A /\ U. U. A e. _V ) -> dom A e. _V )
7	5, 6	mpan 670	. 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 1762   _Vcvv 3106   u. cun 3467   C_ wss 3469   U.cuni 4238   dom cdm 4992   ran crn 4993

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pr 4679  ax-un 6567

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-rex 2813  df-rab 2816  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-opab 4499  df-cnv 5000  df-dm 5002  df-rn 5003

This theorem is referenced by:  dmex  6707  iprc  6709  exse2  6713  xpexr2  6715  xpexcnv  6716  soex  6717  cnvexg  6720  coexg  6725  dmfex  6732  cofunexg  6738  offval3  6768  suppval  6893  funsssuppss  6916  suppss  6920  suppssov1  6922  suppssfv  6926  tposexg  6959  tfrlem12  7048  tfrlem13  7049  erexb  7326  oion  7950  unxpwdom2  8003  wemapwe  8128  wemapweOLD  8129  imadomg  8901  fpwwe2lem3  9000  fpwwe2lem12  9008  fpwwe2lem13  9009  hashfn  12398  hashimarn  12449  o1of2  13384  prdsplusg  14702  prdsmulr  14703  prdsvsca  14704  prdshom  14711  ssclem  15038  ssc2  15041  ssctr  15044  subsubc  15069  resf1st  15110  resf2nd  15111  funcres  15112  efgrcl  16522  dprddomprc  16815  dprdval0prc  16817  dprdgrp  16822  dprdf  16823  dprdcntz  16825  dprddisj  16826  dprdw  16827  dprdwOLD  16833  dprdssv  16839  dprdfeq0  16845  dprdf11  16846  dprdfidOLD  16847  dprdfinvOLD  16849  dprdfaddOLD  16850  dprdfsubOLD  16851  dprdfeq0OLD  16852  dprdf11OLD  16853  dprdres  16858  dprdf1o  16862  subgdmdprd  16864  dmdprdsplitlemOLD  16868  dprddisj2OLD  16871  dprd2da  16874  dmdprdsplit2  16878  dpjfval  16887  dpjidclOLD  16897  f1lindf  18617  decpmatval0  19025  pmatcollpw3lem  19044  ordtbaslem  19448  ordtuni  19450  ordtbas2  19451  ordtbas  19452  ordttopon  19453  ordtopn1  19454  ordtopn2  19455  ordtrest2lem  19463  ordtrest2  19464  txindislem  19862  ordthmeolem  20030  ptcmplem2  20281  tuslem  20498  mbfmulc2re  21783  mbfneg  21785  dvnff  22054  dchrptlem3  23262  fiusgraedgfi  24069  sizeusglecusg  24148  wlks  24181  wlkres  24184  trls  24200  crcts  24284  cycls  24285  vdusgraval  24569  vdgrnn0pnf  24571  hashnbgravdg  24575  usgravd0nedg  24580  iseupa  24627  vdgn0frgrav2  24687  vdgn1frgrav2  24689  vdgfrgragt2  24690  ismgm  24984  ofcfval3  27727  braew  27840  omsval  27890  sibfof  27908  cndprobval  27998  bdayval  28971  bdayfo  28998  tailf  29783  tailfb  29785  f1vrnfibi  31737