Theorem rnexg 7725

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 7571	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7571	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun2 4103	. . . 4 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5868	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3926	. . 3 ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5242	. . 3 ⊢ ((ran 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → ran 𝐴 ∈ V)
7	5, 6	mpan 686	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → ran 𝐴 ∈ V)
8	1, 2, 7	3syl 18	1 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2108  Vcvv 3422   ∪ cun 3881   ⊆ wss 3883  ∪ cuni 4836  dom cdm 5580  ran crn 5581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-cnv 5588  df-dm 5590  df-rn 5591

This theorem is referenced by:  rnex  7733  imaexg  7736  xpexr  7739  xpexr2  7740  soex  7742  cnvexg  7745  coexg  7750  cofunexg  7765  funrnex  7770  abrexexg  7777  tposexg  8027  iunon  8141  onoviun  8145  tz7.44lem1  8207  tz7.44-3  8210  fopwdom  8820  disjen  8870  domss2  8872  domssex  8874  hartogslem2  9232  djuexb  9598  dfac12lem2  9831  unirnfdomd  10254  focdmex  13993  hashimarn  14083  trclexlem  14633  relexp0g  14661  relexpsucnnr  14664  restval  17054  prdsbas  17085  prdsplusg  17086  prdsmulr  17087  prdsvsca  17088  prdshom  17095  sscpwex  17444  sylow1lem4  19121  sylow3lem2  19148  sylow3lem3  19149  lsmvalx  19159  txindislem  22692  xkoptsub  22713  fmfnfmlem3  23015  fmfnfmlem4  23016  ustuqtoplem  23299  ustuqtop0  23300  utopsnneiplem  23307  efabl  25611  efsubm  25612  perpln1  26975  perpln2  26976  isperp  26977  lmif  27050  islmib  27052  isgrpo  28760  grpoinvfval  28785  grpodivfval  28797  isvcOLD  28842  isnv  28875  abrexexd  30755  acunirnmpt  30898  acunirnmpt2  30899  acunirnmpt2f  30900  fnpreimac  30910  locfinreflem  31692  esumrnmpt2  31936  sxsigon  32060  omssubadd  32167  carsgclctunlem2  32186  pmeasadd  32192  sitgclg  32209  bnj1366  32709  ttrclexg  33709  ptrest  35703  elghomlem1OLD  35970  elghomlem2OLD  35971  isrngod  35983  iscringd  36083  imaexALTV  36392  xrnresex  36459  dfcnvrefrels2  36571  dfcnvrefrels3  36572  sticksstones3  40032  lmhmlnmsplit  40828  rclexi  41112  rtrclexlem  41113  trclubgNEW  41115  cnvrcl0  41122  dfrtrcl5  41126  relexpmulg  41207  relexp01min  41210  relexpxpmin  41214  unirnmap  42637  unirnmapsn  42643  ssmapsn  42645  fourierdlem70  43607  fourierdlem71  43608  fourierdlem80  43617  meadjiunlem  43893  omeiunle  43945  fexafv2ex  44599