Theorem rnexg 7842

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 7683	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7683	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun2 4129	. . . 4 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5921	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3941	. . 3 ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5266	. . 3 ⊢ ((ran 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → ran 𝐴 ∈ V)
7	5, 6	mpan 690	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → ran 𝐴 ∈ V)
8	1, 2, 7	3syl 18	1 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2113  Vcvv 3438   ∪ cun 3897   ⊆ wss 3899  ∪ cuni 4861  dom cdm 5622  ran crn 5623

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375  ax-un 7678

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-cnv 5630  df-dm 5632  df-rn 5633

This theorem is referenced by:  rnex  7850  imaexg  7853  rnexd  7855  xpexr  7858  xpexr2  7859  soex  7861  cnvexg  7864  coexg  7869  cofunexg  7891  funrnex  7896  tposexg  8180  iunon  8269  onoviun  8273  tz7.44lem1  8334  tz7.44-3  8337  fopwdom  9011  disjen  9060  domss2  9062  domssex  9064  hartogslem2  9446  ttrclexg  9630  djuexb  9819  dfac12lem2  10053  unirnfdomd  10476  hashimarn  14361  trclexlem  14915  relexp0g  14943  relexpsucnnr  14946  restval  17344  prdsbas  17375  prdsplusg  17376  prdsmulr  17377  prdsvsca  17378  prdshom  17385  sscpwex  17737  sylow1lem4  19528  sylow3lem2  19555  sylow3lem3  19556  lsmvalx  19566  txindislem  23575  xkoptsub  23596  fmfnfmlem3  23898  fmfnfmlem4  23899  ustuqtoplem  24181  ustuqtop0  24182  utopsnneiplem  24189  efabl  26513  efsubm  26514  addsuniflem  27971  ssltmul1  28116  ssltmul2  28117  precsexlem11  28185  perpln1  28731  perpln2  28732  isperp  28733  lmif  28806  islmib  28808  isgrpo  30521  grpoinvfval  30546  grpodivfval  30558  isvcOLD  30603  isnv  30636  abrexexd  32533  acunirnmpt  32686  acunirnmpt2  32687  acunirnmpt2f  32688  fnpreimac  32698  locfinreflem  33946  esumrnmpt2  34174  sxsigon  34298  omssubadd  34406  carsgclctunlem2  34425  pmeasadd  34431  sitgclg  34448  bnj1366  34934  ptrest  37759  elghomlem1OLD  38025  elghomlem2OLD  38026  isrngod  38038  iscringd  38138  xrnresex  38553  dfcnvrefrels2  38720  dfcnvrefrels3  38721  sticksstones3  42341  lmhmlnmsplit  43271  rclexi  43798  rtrclexlem  43799  trclubgNEW  43801  cnvrcl0  43808  dfrtrcl5  43812  relexpmulg  43893  relexp01min  43896  relexpxpmin  43900  unirnmap  45394  unirnmapsn  45400  ssmapsn  45402  fourierdlem70  46362  fourierdlem71  46363  fourierdlem80  46372  meadjiunlem  46651  omeiunle  46703  fexafv2ex  47408