Theorem rnexg 7359

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	⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)

Proof of Theorem rnexg

Step	Hyp	Ref	Expression
1		uniexg 7215	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7215	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun2 4004	. . . 4 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5617	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3836	. . 3 ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5029	. . 3 ⊢ ((ran 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → ran 𝐴 ∈ V)
7	5, 6	mpan 681	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → ran 𝐴 ∈ V)
8	1, 2, 7	3syl 18	1 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2164  Vcvv 3414   ∪ cun 3796   ⊆ wss 3798  ∪ cuni 4658  dom cdm 5342  ran crn 5343

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pr 5127  ax-un 7209

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-rex 3123  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4659  df-br 4874  df-opab 4936  df-cnv 5350  df-dm 5352  df-rn 5353

This theorem is referenced by:  rnex  7362  imaexg  7365  xpexr  7368  xpexr2  7369  soex  7371  cnvexg  7374  coexg  7379  cofunexg  7392  funrnex  7395  abrexexg  7402  tposexg  7631  iunon  7702  onoviun  7706  tz7.44lem1  7767  tz7.44-3  7770  fopwdom  8337  disjen  8386  domss2  8388  domssex  8390  hartogslem2  8717  dfac12lem2  9281  unirnfdomd  9704  focdmex  13431  hashimarn  13516  trclexlem  14112  relexp0g  14139  relexpsucnnr  14142  restval  16440  prdsbas  16470  prdsplusg  16471  prdsmulr  16472  prdsvsca  16473  prdshom  16480  sscpwex  16827  sylow1lem4  18367  sylow3lem2  18394  sylow3lem3  18395  lsmvalx  18405  txindislem  21807  xkoptsub  21828  fmfnfmlem3  22130  fmfnfmlem4  22131  ustuqtoplem  22413  ustuqtop0  22414  utopsnneiplem  22421  efabl  24696  efsubm  24697  perpln1  26022  perpln2  26023  isperp  26024  lmif  26094  islmib  26096  isgrpo  27896  grpoinvfval  27921  grpodivfval  27933  isvcOLD  27978  isnv  28011  abrexexd  29884  acunirnmpt  29997  acunirnmpt2  29998  acunirnmpt2f  29999  locfinreflem  30441  esumrnmpt2  30664  sxsigon  30789  omssubadd  30896  carsgclctunlem2  30915  pmeasadd  30921  sitgclg  30938  bnj1366  31435  ptrest  33945  elghomlem1OLD  34219  elghomlem2OLD  34220  isrngod  34232  iscringd  34332  xrnresex  34705  dfcnvrefrels2  34817  dfcnvrefrels3  34818  lmhmlnmsplit  38493  rclexi  38756  rtrclexlem  38757  trclubgNEW  38759  cnvrcl0  38766  dfrtrcl5  38770  relexpmulg  38836  relexp01min  38839  relexpxpmin  38843  unirnmap  40199  unirnmapsn  40205  ssmapsn  40207  fourierdlem70  41180  fourierdlem71  41181  fourierdlem80  41190  meadjiunlem  41466  omeiunle  41518  fexafv2ex  42115