Theorem rnexg 6613

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 6480	. 2 |- ( A e. V -> U. A e. _V )
2		uniexg 6480	. 2 |- ( U. A e. _V -> U. U. A e. _V )
3		ssun2 3621	. . . 4 |- ran A C_ ( dom A u. ran A )
4		dmrnssfld 5199	. . . 4 |- ( dom A u. ran A ) C_ U. U. A
5	3, 4	sstri 3466	. . 3 |- ran A C_ U. U. A
6		ssexg 4539	. . 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 1758   _Vcvv 3071   u. cun 3427   C_ wss 3429   U.cuni 4192   dom cdm 4941   ran crn 4942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-sep 4514  ax-nul 4522  ax-pr 4632  ax-un 6475

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-mo 2265  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-rex 2801  df-rab 2804  df-v 3073  df-dif 3432  df-un 3434  df-in 3436  df-ss 3443  df-nul 3739  df-if 3893  df-sn 3979  df-pr 3981  df-op 3985  df-uni 4193  df-br 4394  df-opab 4452  df-cnv 4949  df-dm 4951  df-rn 4952

This theorem is referenced by:  rnex  6615  imaexg  6618  xpexr  6621  xpexr2  6622  soex  6624  cnvexg  6627  coexg  6631  cofunexg  6644  funrnex  6647  abrexexg  6655  tposexg  6862  iunon  6902  onoviun  6907  tz7.44lem1  6964  tz7.44-3  6967  fopwdom  7522  disjen  7571  domss2  7573  domssex  7575  hartogslem2  7861  dfac12lem2  8417  unirnfdomd  8835  hashf1rn  12233  hashimarn  12311  restval  14476  prdsbas  14506  prdsplusg  14507  prdsmulr  14508  prdsvsca  14509  prdshom  14516  sscpwex  14839  sylow1lem4  16213  sylow3lem2  16240  sylow3lem3  16241  lsmvalx  16251  txindislem  19331  xkoptsub  19352  fmfnfmlem3  19654  fmfnfmlem4  19655  ustuqtoplem  19939  ustuqtop0  19940  utopsnneiplem  19947  perpln1  23239  perpln2  23240  isperp  23241  sizeusglecusg  23539  isgrpo  23828  grpoinvfval  23856  grpodivfval  23874  gxfval  23889  issubgoi  23942  elghomlem1  23993  elghomlem2  23994  ghgrp  24000  isrngod  24011  isvc  24104  isnv  24135  abrexexd  26035  sxsigon  26744  sitgclg  26865  ptrest  28566  iscringd  28940  lmhmlnmsplit  29581  bnj1366  32126