Theorem rnexg 7896

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 7732	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7732	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun2 4154	. . . 4 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5953	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3968	. . 3 ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5293	. . 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 2108  Vcvv 3459   ∪ cun 3924   ⊆ wss 3926  ∪ cuni 4883  dom cdm 5654  ran crn 5655

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-un 7727

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 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-cnv 5662  df-dm 5664  df-rn 5665

This theorem is referenced by:  rnex  7904  imaexg  7907  rnexd  7909  xpexr  7912  xpexr2  7913  soex  7915  cnvexg  7918  coexg  7923  cofunexg  7945  funrnex  7950  abrexexgOLD  7958  tposexg  8237  iunon  8351  onoviun  8355  tz7.44lem1  8417  tz7.44-3  8420  fopwdom  9092  disjen  9146  domss2  9148  domssex  9150  hartogslem2  9555  ttrclexg  9735  djuexb  9921  dfac12lem2  10157  unirnfdomd  10579  hashimarn  14456  trclexlem  15011  relexp0g  15039  relexpsucnnr  15042  restval  17438  prdsbas  17469  prdsplusg  17470  prdsmulr  17471  prdsvsca  17472  prdshom  17479  sscpwex  17826  sylow1lem4  19580  sylow3lem2  19607  sylow3lem3  19608  lsmvalx  19618  txindislem  23569  xkoptsub  23590  fmfnfmlem3  23892  fmfnfmlem4  23893  ustuqtoplem  24176  ustuqtop0  24177  utopsnneiplem  24184  efabl  26509  efsubm  26510  addsuniflem  27951  ssltmul1  28090  ssltmul2  28091  precsexlem11  28158  perpln1  28635  perpln2  28636  isperp  28637  lmif  28710  islmib  28712  isgrpo  30424  grpoinvfval  30449  grpodivfval  30461  isvcOLD  30506  isnv  30539  abrexexd  32436  acunirnmpt  32583  acunirnmpt2  32584  acunirnmpt2f  32585  fnpreimac  32595  locfinreflem  33817  esumrnmpt2  34045  sxsigon  34169  omssubadd  34278  carsgclctunlem2  34297  pmeasadd  34303  sitgclg  34320  bnj1366  34806  ptrest  37589  elghomlem1OLD  37855  elghomlem2OLD  37856  isrngod  37868  iscringd  37968  imaexALTV  38294  xrnresex  38370  dfcnvrefrels2  38492  dfcnvrefrels3  38493  sticksstones3  42107  lmhmlnmsplit  43058  rclexi  43586  rtrclexlem  43587  trclubgNEW  43589  cnvrcl0  43596  dfrtrcl5  43600  relexpmulg  43681  relexp01min  43684  relexpxpmin  43688  unirnmap  45180  unirnmapsn  45186  ssmapsn  45188  fourierdlem70  46153  fourierdlem71  46154  fourierdlem80  46163  meadjiunlem  46442  omeiunle  46494  fexafv2ex  47197