Theorem rnexg 6706

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 6572	. 2 |- ( A e. V -> U. A e. _V )
2		uniexg 6572	. 2 |- ( U. A e. _V -> U. U. A e. _V )
3		ssun2 3661	. . . 4 |- ran 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 |- ran A C_ U. U. A
6		ssexg 4586	. . 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 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:  rnex  6708  imaexg  6711  xpexr  6714  xpexr2  6715  soex  6717  cnvexg  6720  coexg  6725  cofunexg  6738  funrnex  6741  abrexexg  6749  tposexg  6959  iunon  6999  onoviun  7004  tz7.44lem1  7061  tz7.44-3  7064  fopwdom  7615  disjen  7664  domss2  7666  domssex  7668  hartogslem2  7957  dfac12lem2  8513  unirnfdomd  8931  hashf1rn  12380  hashimarn  12449  restval  14671  prdsbas  14701  prdsplusg  14702  prdsmulr  14703  prdsvsca  14704  prdshom  14711  sscpwex  15034  sylow1lem4  16410  sylow3lem2  16437  sylow3lem3  16438  lsmvalx  16448  txindislem  19862  xkoptsub  19883  fmfnfmlem3  20185  fmfnfmlem4  20186  ustuqtoplem  20470  ustuqtop0  20471  utopsnneiplem  20478  perpln1  23788  perpln2  23789  isperp  23790  lmif  23821  islmib  23823  sizeusglecusg  24148  isgrpo  24724  grpoinvfval  24752  grpodivfval  24770  gxfval  24785  issubgoi  24838  elghomlem1  24889  elghomlem2  24890  ghgrp  24896  isrngod  24907  isvc  25000  isnv  25031  abrexexd  26931  sxsigon  27653  sitgclg  27774  ptrest  29476  iscringd  29850  lmhmlnmsplit  30490  fourierdlem70  31296  fourierdlem71  31297  fourierdlem80  31306  bnj1366  32842