Theorem rnexg 7878

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 7716	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7716	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun2 4142	. . . 4 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5937	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3956	. . 3 ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5278	. . 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 2109  Vcvv 3447   ∪ cun 3912   ⊆ wss 3914  ∪ cuni 4871  dom cdm 5638  ran crn 5639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-cnv 5646  df-dm 5648  df-rn 5649

This theorem is referenced by:  rnex  7886  imaexg  7889  rnexd  7891  xpexr  7894  xpexr2  7895  soex  7897  cnvexg  7900  coexg  7905  cofunexg  7927  funrnex  7932  abrexexgOLD  7940  tposexg  8219  iunon  8308  onoviun  8312  tz7.44lem1  8373  tz7.44-3  8376  fopwdom  9049  disjen  9098  domss2  9100  domssex  9102  hartogslem2  9496  ttrclexg  9676  djuexb  9862  dfac12lem2  10098  unirnfdomd  10520  hashimarn  14405  trclexlem  14960  relexp0g  14988  relexpsucnnr  14991  restval  17389  prdsbas  17420  prdsplusg  17421  prdsmulr  17422  prdsvsca  17423  prdshom  17430  sscpwex  17777  sylow1lem4  19531  sylow3lem2  19558  sylow3lem3  19559  lsmvalx  19569  txindislem  23520  xkoptsub  23541  fmfnfmlem3  23843  fmfnfmlem4  23844  ustuqtoplem  24127  ustuqtop0  24128  utopsnneiplem  24135  efabl  26459  efsubm  26460  addsuniflem  27908  ssltmul1  28050  ssltmul2  28051  precsexlem11  28119  perpln1  28637  perpln2  28638  isperp  28639  lmif  28712  islmib  28714  isgrpo  30426  grpoinvfval  30451  grpodivfval  30463  isvcOLD  30508  isnv  30541  abrexexd  32438  acunirnmpt  32583  acunirnmpt2  32584  acunirnmpt2f  32585  fnpreimac  32595  locfinreflem  33830  esumrnmpt2  34058  sxsigon  34182  omssubadd  34291  carsgclctunlem2  34310  pmeasadd  34316  sitgclg  34333  bnj1366  34819  ptrest  37613  elghomlem1OLD  37879  elghomlem2OLD  37880  isrngod  37892  iscringd  37992  xrnresex  38392  dfcnvrefrels2  38519  dfcnvrefrels3  38520  sticksstones3  42136  lmhmlnmsplit  43076  rclexi  43604  rtrclexlem  43605  trclubgNEW  43607  cnvrcl0  43614  dfrtrcl5  43618  relexpmulg  43699  relexp01min  43702  relexpxpmin  43706  unirnmap  45202  unirnmapsn  45208  ssmapsn  45210  fourierdlem70  46174  fourierdlem71  46175  fourierdlem80  46184  meadjiunlem  46463  omeiunle  46515  fexafv2ex  47221