Theorem rnexg 5090

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 4665	. 2 |- ( A e. V -> U. A e. _V )
2		uniexg 4665	. 2 |- ( U. A e. _V -> U. U. A e. _V )
3		ssun2 3471	. . . 4 |- ran A C_ ( dom A u. ran A )
4		dmrnssfld 5088	. . . 4 |- ( dom A u. ran A ) C_ U. U. A
5	3, 4	sstri 3317	. . 3 |- ran A C_ U. U. A
6		ssexg 4309	. . 3 |- ( ( ran A C_ U. U. A /\ U. U. A e. _V ) -> ran A e. _V )
7	5, 6	mpan 652	. 2 |- ( U. U. A e. _V -> ran A e. _V )
8	1, 2, 7	3syl 19	1 |- ( A e. V -> ran A e. _V )

Syntax hints:   -> wi 4   e. wcel 1721   _Vcvv 2916   u. cun 3278   C_ wss 3280   U.cuni 3975   dom cdm 4837   ran crn 4838

This theorem is referenced by:  rnex  5092  imaexg  5176  xpexr  5266  xpexr2  5267  soex  5278  cnvexg  5364  coexg  5371  cofunexg  5918  funrnex  5926  abrexexg  5943  tposexg  6452  iunon  6559  onoviun  6564  tz7.44lem1  6622  tz7.44-3  6625  fopwdom  7175  disjen  7223  domss2  7225  domssex  7227  hartogslem2  7468  dfac12lem2  7980  unirnfdomd  8398  hashf1rn  11591  restval  13609  prdsbas  13635  prdsplusg  13636  prdsmulr  13637  prdsvsca  13638  prdshom  13644  sscpwex  13970  sylow1lem4  15190  sylow3lem2  15217  sylow3lem3  15218  lsmvalx  15228  txindislem  17618  xkoptsub  17639  fmfnfmlem3  17941  fmfnfmlem4  17942  ustuqtoplem  18222  ustuqtop0  18223  utopsnneiplem  18230  sizeusglecusg  21448  isgrpo  21737  grpoinvfval  21765  grpodivfval  21783  gxfval  21798  issubgoi  21851  elghomlem1  21902  elghomlem2  21903  ghgrp  21909  isrngod  21920  isvc  22013  isnv  22044  abrexexd  23943  sxsigon  24499  sitgclg  24609  iscringd  26499  lmhmlnmsplit  27053  hashimarn  27994  bnj1366  28907

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363  ax-un 4660

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-cnv 4845  df-dm 4847  df-rn 4848