Theorem rnexg 6731

Description: The range of a set is a set. Corollary 6.8(3) of [TakeutiZaring] p. 26. Similar to Lemma 3D of [Enderton] p. 41. (Contributed by NM, 31-Mar-1995.)

Assertion

Ref	Expression
rnexg	|- ( A e. V -> ran A e. _V )

Proof of Theorem rnexg

Step	Hyp	Ref	Expression
1		uniexg 6596	. 2 |- ( A e. V -> U. A e. _V )
2		uniexg 6596	. 2 |- ( U. A e. _V -> U. U. A e. _V )
3		ssun2 3664	. . . 4 |- ran A C_ ( dom A u. ran A )
4		dmrnssfld 5271	. . . 4 |- ( dom A u. ran A ) C_ U. U. A
5	3, 4	sstri 3508	. . 3 |- ran A C_ U. U. A
6		ssexg 4602	. . 3 |- ( ( ran A C_ U. U. A /\ U. U. A e. _V ) -> ran A e. _V )
7	5, 6	mpan 670	. 2 |- ( U. U. A e. _V -> ran A e. _V )
8	1, 2, 7	3syl 20	1 |- ( A e. V -> ran A e. _V )

Syntax hints:   -> wi 4   e. wcel 1819   _Vcvv 3109   u. cun 3469   C_ wss 3471   U.cuni 4251   dom cdm 5008   ran crn 5009

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pr 4695  ax-un 6591

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-br 4457  df-opab 4516  df-cnv 5016  df-dm 5018  df-rn 5019

This theorem is referenced by:  rnex  6733  imaexg  6736  xpexr  6739  xpexr2  6740  soex  6742  cnvexg  6745  coexg  6750  cofunexg  6763  funrnex  6766  abrexexg  6774  tposexg  6987  iunon  7027  onoviun  7032  tz7.44lem1  7089  tz7.44-3  7092  fopwdom  7644  disjen  7693  domss2  7695  domssex  7697  hartogslem2  7986  dfac12lem2  8541  unirnfdomd  8959  hashf1rn  12428  hashimarn  12500  restval  14844  prdsbas  14874  prdsplusg  14875  prdsmulr  14876  prdsvsca  14877  prdshom  14884  sscpwex  15231  sylow1lem4  16748  sylow3lem2  16775  sylow3lem3  16776  lsmvalx  16786  txindislem  20260  xkoptsub  20281  fmfnfmlem3  20583  fmfnfmlem4  20584  ustuqtoplem  20868  ustuqtop0  20869  utopsnneiplem  20876  efabl  23063  efsubm  23064  perpln1  24213  perpln2  24214  isperp  24215  lmif  24277  islmib  24279  sizeusglecusg  24613  isgrpo  25325  grpoinvfval  25353  grpodivfval  25371  gxfval  25386  issubgoi  25439  elghomlem1OLD  25490  elghomlem2OLD  25491  ghgrpOLD  25497  isrngod  25508  isvc  25601  isnv  25632  abrexexd  27535  acunirnmpt  27653  acunirnmpt2  27654  acunirnmpt2f  27655  locfinreflem  28004  esumrnmpt2  28240  sxsigon  28336  omssubadd  28444  carsgclctunlem2  28461  sitgclg  28481  relexp0g  29249  relexpsucnnr  29252  ptrest  30253  iscringd  30601  lmhmlnmsplit  31237  fourierdlem70  32162  fourierdlem71  32163  fourierdlem80  32172  bnj1366  34031  trclexlem  37955