Theorem rnexg 7853

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 7694	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7694	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun2 4119	. . . 4 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5929	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3931	. . 3 ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5264	. . 3 ⊢ ((ran 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → ran 𝐴 ∈ V)
7	5, 6	mpan 691	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → ran 𝐴 ∈ V)
8	1, 2, 7	3syl 18	1 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3429   ∪ cun 3887   ⊆ wss 3889  ∪ cuni 4850  dom cdm 5631  ran crn 5632

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-cnv 5639  df-dm 5641  df-rn 5642

This theorem is referenced by:  rnex  7861  imaexg  7864  rnexd  7866  xpexr  7869  xpexr2  7870  soex  7872  cnvexg  7875  coexg  7880  cofunexg  7902  funrnex  7907  tposexg  8190  iunon  8279  onoviun  8283  tz7.44lem1  8344  tz7.44-3  8347  fopwdom  9023  disjen  9072  domss2  9074  domssex  9076  hartogslem2  9458  ttrclexg  9644  djuexb  9833  dfac12lem2  10067  unirnfdomd  10490  hashimarn  14402  trclexlem  14956  relexp0g  14984  relexpsucnnr  14987  restval  17389  prdsbas  17420  prdsplusg  17421  prdsmulr  17422  prdsvsca  17423  prdshom  17430  sscpwex  17782  sylow1lem4  19576  sylow3lem2  19603  sylow3lem3  19604  lsmvalx  19614  txindislem  23598  xkoptsub  23619  fmfnfmlem3  23921  fmfnfmlem4  23922  ustuqtoplem  24204  ustuqtop0  24205  utopsnneiplem  24212  efabl  26514  efsubm  26515  addsuniflem  27993  sltmuls1  28139  sltmuls2  28140  precsexlem11  28209  perpln1  28778  perpln2  28779  isperp  28780  lmif  28853  islmib  28855  isgrpo  30568  grpoinvfval  30593  grpodivfval  30605  isvcOLD  30650  isnv  30683  abrexexd  32579  acunirnmpt  32732  acunirnmpt2  32733  acunirnmpt2f  32734  fnpreimac  32743  locfinreflem  33984  esumrnmpt2  34212  sxsigon  34336  omssubadd  34444  carsgclctunlem2  34463  pmeasadd  34469  sitgclg  34486  bnj1366  34971  ptrest  37940  elghomlem1OLD  38206  elghomlem2OLD  38207  isrngod  38219  iscringd  38319  xrnresex  38750  dfcnvrefrels2  38929  dfcnvrefrels3  38930  eldisjs7  39262  sticksstones3  42587  lmhmlnmsplit  43515  rclexi  44042  rtrclexlem  44043  trclubgNEW  44045  cnvrcl0  44052  dfrtrcl5  44056  relexpmulg  44137  relexp01min  44140  relexpxpmin  44144  unirnmap  45637  unirnmapsn  45643  ssmapsn  45645  fourierdlem70  46604  fourierdlem71  46605  fourierdlem80  46614  meadjiunlem  46893  omeiunle  46945  fexafv2ex  47668