Theorem rnexg 7895

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 7738	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7738	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun2 4132	. . . 4 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5964	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3946	. . 3 ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5290	. . 3 ⊢ ((ran 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → ran 𝐴 ∈ V)
7	5, 6	mpan 702	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → ran 𝐴 ∈ V)
8	1, 2, 7	3syl 19	1 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2143  Vcvv 3455   ∪ cun 3903   ⊆ wss 3905  ∪ cuni 4872  dom cdm 5661  ran crn 5662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-cnv 5669  df-dm 5671  df-rn 5672

This theorem is referenced by:  rnex  7903  imaexg  7906  rnexd  7908  xpexr  7911  xpexr2  7912  soex  7914  cnvexg  7917  coexg  7922  cofunexg  7942  funrnex  7947  tposexg  8232  iunon  8322  onoviun  8326  tz7.44lem1  8388  tz7.44-3  8391  fopwdom  9069  disjen  9118  domss2  9120  domssex  9122  hartogslem2  9501  ttrclexg  9688  djuexb  9891  dfac12lem2  10124  unirnfdomd  10547  hashimarn  14473  trclexlem  15027  relexp0g  15055  relexpsucnnr  15058  restval  17474  prdsbas  17505  prdsplusg  17506  prdsmulr  17507  prdsvsca  17508  prdshom  17515  sscpwex  17867  sylow1lem4  19666  sylow3lem2  19693  sylow3lem3  19694  lsmvalx  19704  txindislem  23790  xkoptsub  23811  fmfnfmlem3  24113  fmfnfmlem4  24114  ustuqtoplem  24396  ustuqtop0  24397  utopsnneiplem  24404  efabl  26715  efsubm  26716  addsuniflem  28194  sltmuls1  28340  sltmuls2  28341  precsexlem11  28410  perpln1  28990  perpln2  28991  isperp  28992  lmif  29094  islmib  29096  isgrpo  30849  grpoinvfval  30874  grpodivfval  30886  isvcOLD  30931  isnv  30964  abrexexd  32855  acunirnmpt  33004  acunirnmpt2  33005  acunirnmpt2f  33006  fnpreimac  33015  locfinreflem  34230  esumrnmpt2  34458  sxsigon  34582  omssubadd  34690  carsgclctunlem2  34709  pmeasadd  34715  sitgclg  34732  bnj1366  35217  ptrest  38290  elghomlem1OLD  38556  elghomlem2OLD  38557  isrngod  38569  iscringd  38669  xrnresex  39098  dfcnvrefrels2  39277  dfcnvrefrels3  39278  eldisjs7  39610  sticksstones3  42935  lmhmlnmsplit  43834  rclexi  44361  rtrclexlem  44362  trclubgNEW  44364  cnvrcl0  44371  dfrtrcl5  44375  relexpmulg  44456  relexp01min  44459  relexpxpmin  44463  unirnmap  45944  unirnmapsn  45950  ssmapsn  45952  fourierdlem70  46910  fourierdlem71  46911  fourierdlem80  46920  meadjiunlem  47199  omeiunle  47251  fexafv2ex  47977