Theorem rnexg 6713

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 6578	. 2 |- ( A e. V -> U. A e. _V )
2		uniexg 6578	. 2 |- ( U. A e. _V -> U. U. A e. _V )
3		ssun2 3650	. . . 4 |- ran A C_ ( dom A u. ran A )
4		dmrnssfld 5247	. . . 4 |- ( dom A u. ran A ) C_ U. U. A
5	3, 4	sstri 3495	. . 3 |- ran A C_ U. U. A
6		ssexg 4579	. . 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 1802   _Vcvv 3093   u. cun 3456   C_ wss 3458   U.cuni 4230   dom cdm 4985   ran crn 4986

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-sep 4554  ax-nul 4562  ax-pr 4672  ax-un 6573

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 974  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-rex 2797  df-rab 2800  df-v 3095  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-nul 3768  df-if 3923  df-sn 4011  df-pr 4013  df-op 4017  df-uni 4231  df-br 4434  df-opab 4492  df-cnv 4993  df-dm 4995  df-rn 4996

This theorem is referenced by:  rnex  6715  imaexg  6718  xpexr  6721  xpexr2  6722  soex  6724  cnvexg  6727  coexg  6732  cofunexg  6745  funrnex  6748  abrexexg  6756  tposexg  6967  iunon  7007  onoviun  7012  tz7.44lem1  7069  tz7.44-3  7072  fopwdom  7623  disjen  7672  domss2  7674  domssex  7676  hartogslem2  7966  dfac12lem2  8522  unirnfdomd  8940  hashf1rn  12399  hashimarn  12470  restval  14696  prdsbas  14726  prdsplusg  14727  prdsmulr  14728  prdsvsca  14729  prdshom  14736  sscpwex  15056  sylow1lem4  16490  sylow3lem2  16517  sylow3lem3  16518  lsmvalx  16528  txindislem  20000  xkoptsub  20021  fmfnfmlem3  20323  fmfnfmlem4  20324  ustuqtoplem  20608  ustuqtop0  20609  utopsnneiplem  20616  efabl  22802  efsubm  22803  perpln1  23952  perpln2  23953  isperp  23954  lmif  24016  islmib  24018  sizeusglecusg  24351  isgrpo  25063  grpoinvfval  25091  grpodivfval  25109  gxfval  25124  issubgoi  25177  elghomlem1OLD  25228  elghomlem2OLD  25229  ghgrpOLD  25235  isrngod  25246  isvc  25339  isnv  25370  abrexexd  27272  locfinreflem  27709  sxsigon  28029  sitgclg  28150  ptrest  30016  iscringd  30364  lmhmlnmsplit  31001  fourierdlem70  31844  fourierdlem71  31845  fourierdlem80  31854  bnj1366  33595