Theorem rnexg 7595

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 7446	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7446	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun2 4100	. . . 4 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5806	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3924	. . 3 ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5191	. . 3 ⊢ ((ran 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → ran 𝐴 ∈ V)
7	5, 6	mpan 689	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → ran 𝐴 ∈ V)
8	1, 2, 7	3syl 18	1 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2111  Vcvv 3441   ∪ cun 3879   ⊆ wss 3881  ∪ cuni 4800  dom cdm 5519  ran crn 5520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-cnv 5527  df-dm 5529  df-rn 5530

This theorem is referenced by:  rnex  7599  imaexg  7602  xpexr  7605  xpexr2  7606  soex  7608  cnvexg  7611  coexg  7616  cofunexg  7632  funrnex  7637  abrexexg  7644  tposexg  7889  iunon  7959  onoviun  7963  tz7.44lem1  8024  tz7.44-3  8027  fopwdom  8608  disjen  8658  domss2  8660  domssex  8662  hartogslem2  8991  djuexb  9322  dfac12lem2  9555  unirnfdomd  9978  focdmex  13707  hashimarn  13797  trclexlem  14345  relexp0g  14373  relexpsucnnr  14376  restval  16692  prdsbas  16722  prdsplusg  16723  prdsmulr  16724  prdsvsca  16725  prdshom  16732  sscpwex  17077  sylow1lem4  18718  sylow3lem2  18745  sylow3lem3  18746  lsmvalx  18756  txindislem  22238  xkoptsub  22259  fmfnfmlem3  22561  fmfnfmlem4  22562  ustuqtoplem  22845  ustuqtop0  22846  utopsnneiplem  22853  efabl  25142  efsubm  25143  perpln1  26504  perpln2  26505  isperp  26506  lmif  26579  islmib  26581  isgrpo  28280  grpoinvfval  28305  grpodivfval  28317  isvcOLD  28362  isnv  28395  abrexexd  30277  acunirnmpt  30422  acunirnmpt2  30423  acunirnmpt2f  30424  fnpreimac  30434  locfinreflem  31193  esumrnmpt2  31437  sxsigon  31561  omssubadd  31668  carsgclctunlem2  31687  pmeasadd  31693  sitgclg  31710  bnj1366  32211  ptrest  35056  elghomlem1OLD  35323  elghomlem2OLD  35324  isrngod  35336  iscringd  35436  imaexALTV  35747  xrnresex  35814  dfcnvrefrels2  35926  dfcnvrefrels3  35927  lmhmlnmsplit  40031  rclexi  40315  rtrclexlem  40316  trclubgNEW  40318  cnvrcl0  40325  dfrtrcl5  40329  relexpmulg  40411  relexp01min  40414  relexpxpmin  40418  unirnmap  41837  unirnmapsn  41843  ssmapsn  41845  fourierdlem70  42818  fourierdlem71  42819  fourierdlem80  42828  meadjiunlem  43104  omeiunle  43156  fexafv2ex  43776