Theorem rnexg 6505

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 6372	. 2 |- ( A e. V -> U. A e. _V )
2		uniexg 6372	. 2 |- ( U. A e. _V -> U. U. A e. _V )
3		ssun2 3515	. . . 4 |- ran A C_ ( dom A u. ran A )
4		dmrnssfld 5093	. . . 4 |- ( dom A u. ran A ) C_ U. U. A
5	3, 4	sstri 3360	. . 3 |- ran A C_ U. U. A
6		ssexg 4433	. . 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 1756   _Vcvv 2967   u. cun 3321   C_ wss 3323   U.cuni 4086   dom cdm 4835   ran crn 4836

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 2419  ax-sep 4408  ax-nul 4416  ax-pr 4526  ax-un 6367

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 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-rex 2716  df-rab 2719  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-if 3787  df-sn 3873  df-pr 3875  df-op 3879  df-uni 4087  df-br 4288  df-opab 4346  df-cnv 4843  df-dm 4845  df-rn 4846

This theorem is referenced by:  rnex  6507  imaexg  6510  xpexr  6513  xpexr2  6514  soex  6516  cnvexg  6519  coexg  6523  cofunexg  6536  funrnex  6539  abrexexg  6547  tposexg  6754  iunon  6791  onoviun  6796  tz7.44lem1  6853  tz7.44-3  6856  fopwdom  7411  disjen  7460  domss2  7462  domssex  7464  hartogslem2  7749  dfac12lem2  8305  unirnfdomd  8723  hashf1rn  12115  hashimarn  12192  restval  14357  prdsbas  14387  prdsplusg  14388  prdsmulr  14389  prdsvsca  14390  prdshom  14397  sscpwex  14720  sylow1lem4  16091  sylow3lem2  16118  sylow3lem3  16119  lsmvalx  16129  txindislem  19181  xkoptsub  19202  fmfnfmlem3  19504  fmfnfmlem4  19505  ustuqtoplem  19789  ustuqtop0  19790  utopsnneiplem  19797  sizeusglecusg  23345  isgrpo  23634  grpoinvfval  23662  grpodivfval  23680  gxfval  23695  issubgoi  23748  elghomlem1  23799  elghomlem2  23800  ghgrp  23806  isrngod  23817  isvc  23910  isnv  23941  abrexexd  25841  sxsigon  26558  sitgclg  26680  ptrest  28378  iscringd  28752  lmhmlnmsplit  29393  bnj1366  31710