Theorem dmexg 6512

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 6380	. 2 |- ( A e. V -> U. A e. _V )
2		uniexg 6380	. 2 |- ( U. A e. _V -> U. U. A e. _V )
3		ssun1 3522	. . . 4 |- dom A C_ ( dom A u. ran A )
4		dmrnssfld 5101	. . . 4 |- ( dom A u. ran A ) C_ U. U. A
5	3, 4	sstri 3368	. . 3 |- dom A C_ U. U. A
6		ssexg 4441	. . 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 1756   _Vcvv 2975   u. cun 3329   C_ wss 3331   U.cuni 4094   dom cdm 4843   ran crn 4844

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4416  ax-nul 4424  ax-pr 4534  ax-un 6375

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-ne 2611  df-rex 2724  df-rab 2727  df-v 2977  df-dif 3334  df-un 3336  df-in 3338  df-ss 3345  df-nul 3641  df-if 3795  df-sn 3881  df-pr 3883  df-op 3887  df-uni 4095  df-br 4296  df-opab 4354  df-cnv 4851  df-dm 4853  df-rn 4854

This theorem is referenced by:  dmex  6514  iprc  6516  exse2  6520  xpexr2  6522  xpexcnv  6523  soex  6524  cnvexg  6527  coexg  6531  dmfex  6538  cofunexg  6544  offval3  6574  suppval  6695  funsssuppss  6718  suppss  6722  suppssov1  6724  suppssfv  6728  tposexg  6762  tfrlem12  6851  tfrlem13  6852  erexb  7129  oion  7753  unxpwdom2  7806  wemapwe  7931  wemapweOLD  7932  imadomg  8704  fpwwe2lem3  8803  fpwwe2lem12  8811  fpwwe2lem13  8812  hashfn  12141  hashimarn  12203  o1of2  13093  prdsplusg  14399  prdsmulr  14400  prdsvsca  14401  prdshom  14408  ssclem  14735  ssc2  14738  ssctr  14741  subsubc  14766  resf1st  14807  resf2nd  14808  funcres  14809  efgrcl  16215  dprddomprc  16485  dprdval0prc  16487  dprdgrp  16492  dprdf  16493  dprdcntz  16495  dprddisj  16496  dprdw  16497  dprdwOLD  16503  dprdssv  16509  dprdfeq0  16515  dprdf11  16516  dprdfidOLD  16517  dprdfinvOLD  16519  dprdfaddOLD  16520  dprdfsubOLD  16521  dprdfeq0OLD  16522  dprdf11OLD  16523  dprdres  16528  dprdf1o  16532  subgdmdprd  16534  dmdprdsplitlemOLD  16538  dprddisj2OLD  16541  dprd2da  16544  dmdprdsplit2  16548  dpjfval  16557  dpjidclOLD  16567  f1lindf  18254  ordtbaslem  18795  ordtuni  18797  ordtbas2  18798  ordtbas  18799  ordttopon  18800  ordtopn1  18801  ordtopn2  18802  ordtrest2lem  18810  ordtrest2  18811  txindislem  19209  ordthmeolem  19377  ptcmplem2  19628  tuslem  19845  mbfmulc2re  21129  mbfneg  21131  dvnff  21400  dchrptlem3  22608  fiusgraedgfi  23323  sizeusglecusg  23397  wlks  23428  wlkres  23431  trls  23438  crcts  23511  cycls  23512  vdusgraval  23580  vdgrnn0pnf  23582  hashnbgravdg  23584  usgravd0nedg  23585  iseupa  23589  ismgm  23810  ofcfval3  26547  braew  26661  omsval  26711  sibfof  26729  cndprobval  26819  bdayval  27792  bdayfo  27819  tailf  28599  tailfb  28601  vdgn0frgrav2  30620  vdgn1frgrav2  30622  vdgfrgragt2  30623