Theorem rnexg 7847

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 7688	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7688	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun2 4120	. . . 4 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5924	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3932	. . 3 ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5261	. . 3 ⊢ ((ran 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → ran 𝐴 ∈ V)
7	5, 6	mpan 691	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → ran 𝐴 ∈ V)
8	1, 2, 7	3syl 18	1 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3430   ∪ cun 3888   ⊆ wss 3890  ∪ cuni 4851  dom cdm 5625  ran crn 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232  ax-pr 5371  ax-un 7683

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-cnv 5633  df-dm 5635  df-rn 5636

This theorem is referenced by:  rnex  7855  imaexg  7858  rnexd  7860  xpexr  7863  xpexr2  7864  soex  7866  cnvexg  7869  coexg  7874  cofunexg  7896  funrnex  7901  tposexg  8184  iunon  8273  onoviun  8277  tz7.44lem1  8338  tz7.44-3  8341  fopwdom  9017  disjen  9066  domss2  9068  domssex  9070  hartogslem2  9452  ttrclexg  9638  djuexb  9827  dfac12lem2  10061  unirnfdomd  10484  hashimarn  14396  trclexlem  14950  relexp0g  14978  relexpsucnnr  14981  restval  17383  prdsbas  17414  prdsplusg  17415  prdsmulr  17416  prdsvsca  17417  prdshom  17424  sscpwex  17776  sylow1lem4  19570  sylow3lem2  19597  sylow3lem3  19598  lsmvalx  19608  txindislem  23611  xkoptsub  23632  fmfnfmlem3  23934  fmfnfmlem4  23935  ustuqtoplem  24217  ustuqtop0  24218  utopsnneiplem  24225  efabl  26530  efsubm  26531  addsuniflem  28010  sltmuls1  28156  sltmuls2  28157  precsexlem11  28226  perpln1  28795  perpln2  28796  isperp  28797  lmif  28870  islmib  28872  isgrpo  30586  grpoinvfval  30611  grpodivfval  30623  isvcOLD  30668  isnv  30701  abrexexd  32597  acunirnmpt  32750  acunirnmpt2  32751  acunirnmpt2f  32752  fnpreimac  32761  locfinreflem  34003  esumrnmpt2  34231  sxsigon  34355  omssubadd  34463  carsgclctunlem2  34482  pmeasadd  34488  sitgclg  34505  bnj1366  34990  ptrest  37957  elghomlem1OLD  38223  elghomlem2OLD  38224  isrngod  38236  iscringd  38336  xrnresex  38767  dfcnvrefrels2  38946  dfcnvrefrels3  38947  eldisjs7  39279  sticksstones3  42604  lmhmlnmsplit  43536  rclexi  44063  rtrclexlem  44064  trclubgNEW  44066  cnvrcl0  44073  dfrtrcl5  44077  relexpmulg  44158  relexp01min  44161  relexpxpmin  44165  unirnmap  45658  unirnmapsn  45664  ssmapsn  45666  fourierdlem70  46625  fourierdlem71  46626  fourierdlem80  46635  meadjiunlem  46914  omeiunle  46966  fexafv2ex  47683