Theorem rnexg 7924

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 7758	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7758	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun2 4188	. . . 4 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5986	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 4004	. . 3 ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5328	. . 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 2105  Vcvv 3477   ∪ cun 3960   ⊆ wss 3962  ∪ cuni 4911  dom cdm 5688  ran crn 5689

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-cnv 5696  df-dm 5698  df-rn 5699

This theorem is referenced by:  rnex  7932  imaexg  7935  rnexd  7937  xpexr  7940  xpexr2  7941  soex  7943  cnvexg  7946  coexg  7951  cofunexg  7971  funrnex  7976  abrexexgOLD  7984  tposexg  8263  iunon  8377  onoviun  8381  tz7.44lem1  8443  tz7.44-3  8446  fopwdom  9118  disjen  9172  domss2  9174  domssex  9176  hartogslem2  9580  ttrclexg  9760  djuexb  9946  dfac12lem2  10182  unirnfdomd  10604  hashimarn  14475  trclexlem  15029  relexp0g  15057  relexpsucnnr  15060  restval  17472  prdsbas  17503  prdsplusg  17504  prdsmulr  17505  prdsvsca  17506  prdshom  17513  sscpwex  17862  sylow1lem4  19633  sylow3lem2  19660  sylow3lem3  19661  lsmvalx  19671  txindislem  23656  xkoptsub  23677  fmfnfmlem3  23979  fmfnfmlem4  23980  ustuqtoplem  24263  ustuqtop0  24264  utopsnneiplem  24271  efabl  26606  efsubm  26607  addsuniflem  28048  ssltmul1  28187  ssltmul2  28188  precsexlem11  28255  perpln1  28732  perpln2  28733  isperp  28734  lmif  28807  islmib  28809  isgrpo  30525  grpoinvfval  30550  grpodivfval  30562  isvcOLD  30607  isnv  30640  abrexexd  32536  acunirnmpt  32675  acunirnmpt2  32676  acunirnmpt2f  32677  fnpreimac  32687  locfinreflem  33800  esumrnmpt2  34048  sxsigon  34172  omssubadd  34281  carsgclctunlem2  34300  pmeasadd  34306  sitgclg  34323  bnj1366  34821  ptrest  37605  elghomlem1OLD  37871  elghomlem2OLD  37872  isrngod  37884  iscringd  37984  imaexALTV  38311  xrnresex  38387  dfcnvrefrels2  38509  dfcnvrefrels3  38510  sticksstones3  42129  lmhmlnmsplit  43075  rclexi  43604  rtrclexlem  43605  trclubgNEW  43607  cnvrcl0  43614  dfrtrcl5  43618  relexpmulg  43699  relexp01min  43702  relexpxpmin  43706  unirnmap  45150  unirnmapsn  45156  ssmapsn  45158  fourierdlem70  46131  fourierdlem71  46132  fourierdlem80  46141  meadjiunlem  46420  omeiunle  46472  fexafv2ex  47169