Theorem rnexg 7918

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 7761	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7761	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun2 4176	. . . 4 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5957	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3918	. . 3 ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5281	. . 3 ⊢ ((ran 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → ran 𝐴 ∈ V)
7	5, 6	mpan 703	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → ran 𝐴 ∈ V)
8	1, 2, 7	3syl 19	1 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144  Vcvv 3450   ⊆ wss 3896   ∪ cun 4148  ∪ cuni 4866  dom cdm 5651  ran crn 5652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5391  ax-un 7755

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-cnv 5659  df-dm 5661  df-rn 5662

This theorem is used by:  rnex  7926  imaexg  7929  rnexd  7931  xpexr  7934  xpexr2  7935  soex  7937  cnvexg  7940  coexg  7945  cofunexg  7965  funrnex  7970  tposexg  8265  iunon  8355  onoviun  8359  tz7.44lem1  8421  tz7.44-3  8424  fopwdom  9112  disjen  9161  domss2  9163  domssex  9165  hartogslem2  9544  ttrclexg  9731  djuexb  9997  dfac12lem2  10230  unirnfdomd  10659  hashimarn  14592  trclexlem  15156  relexp0g  15184  relexpsucnnr  15187  restval  17606  prdsbas  17637  prdsplusg  17638  prdsmulr  17639  prdsvsca  17640  prdshom  17647  sscpwex  17999  sylow1lem4  19824  sylow3lem2  19851  sylow3lem3  19852  lsmvalx  19862  txindislem  23961  xkoptsub  23982  fmfnfmlem3  24284  fmfnfmlem4  24285  ustuqtoplem  24567  ustuqtop0  24568  utopsnneiplem  24575  efabl  26887  efsubm  26888  addsuniflem  28396  sltmuls1  28542  sltmuls2  28543  precsexlem11  28612  perpln1  29194  perpln2  29195  isperp  29196  lmif  29299  islmib  29301  isgrpo  31108  grpoinvfval  31133  grpodivfval  31145  isvcOLD  31190  isnv  31223  abrexexd  33156  acunirnmpt  33304  acunirnmpt2  33305  acunirnmpt2f  33306  fnpreimac  33315  locfinreflem  34522  esumrnmpt2  34750  sxsigon  34875  omssubadd  34982  carsgclctunlem2  35001  pmeasadd  35007  sitgclg  35024  bnj1366  35509  ptrest  38674  elghomlem1OLD  38956  elghomlem2OLD  38957  isrngod  38969  iscringd  39069  xrnresex  39498  dfcnvrefrels2  39677  dfcnvrefrels3  39678  eldisjs7  40010  sticksstones3  43335  lmhmlnmsplit  44226  rclexi  44752  rtrclexlem  44753  trclubgNEW  44755  cnvrcl0  44762  dfrtrcl5  44766  relexpmulg  44847  relexp01min  44850  relexpxpmin  44854  unirnmap  46357  unirnmapsn  46363  ssmapsn  46365  fourierdlem70  47322  fourierdlem71  47323  fourierdlem80  47332  meadjiunlem  47611  omeiunle  47663  fexafv2ex  48426