Theorem rnexg 7842

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 7683	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7683	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun2 4108	. . . 4 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5916	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3924	. . 3 ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5251	. . 3 ⊢ ((ran 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → ran 𝐴 ∈ V)
7	5, 6	mpan 696	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → ran 𝐴 ∈ V)
8	1, 2, 7	3syl 18	1 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2119  Vcvv 3431   ∪ cun 3881   ⊆ wss 3883  ∪ cuni 4838  dom cdm 5618  ran crn 5619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-cnv 5626  df-dm 5628  df-rn 5629

This theorem is referenced by:  rnex  7850  imaexg  7853  rnexd  7855  xpexr  7858  xpexr2  7859  soex  7861  cnvexg  7864  coexg  7869  cofunexg  7891  funrnex  7896  tposexg  8180  iunon  8269  onoviun  8273  tz7.44lem1  8334  tz7.44-3  8337  fopwdom  9013  disjen  9062  domss2  9064  domssex  9066  hartogslem2  9448  ttrclexg  9635  djuexb  9824  dfac12lem2  10058  unirnfdomd  10481  hashimarn  14393  trclexlem  14947  relexp0g  14975  relexpsucnnr  14978  restval  17380  prdsbas  17411  prdsplusg  17412  prdsmulr  17413  prdsvsca  17414  prdshom  17421  sscpwex  17773  sylow1lem4  19567  sylow3lem2  19594  sylow3lem3  19595  lsmvalx  19605  txindislem  23616  xkoptsub  23637  fmfnfmlem3  23939  fmfnfmlem4  23940  ustuqtoplem  24222  ustuqtop0  24223  utopsnneiplem  24230  efabl  26532  efsubm  26533  addsuniflem  28011  sltmuls1  28157  sltmuls2  28158  precsexlem11  28227  perpln1  28796  perpln2  28797  isperp  28798  lmif  28871  islmib  28873  isgrpo  30586  grpoinvfval  30611  grpodivfval  30623  isvcOLD  30668  isnv  30701  abrexexd  32597  acunirnmpt  32751  acunirnmpt2  32752  acunirnmpt2f  32753  fnpreimac  32762  locfinreflem  34024  esumrnmpt2  34252  sxsigon  34376  omssubadd  34484  carsgclctunlem2  34503  pmeasadd  34509  sitgclg  34526  bnj1366  35011  ptrest  37986  elghomlem1OLD  38252  elghomlem2OLD  38253  isrngod  38265  iscringd  38365  xrnresex  38796  dfcnvrefrels2  38975  dfcnvrefrels3  38976  eldisjs7  39308  sticksstones3  42633  lmhmlnmsplit  43532  rclexi  44059  rtrclexlem  44060  trclubgNEW  44062  cnvrcl0  44069  dfrtrcl5  44073  relexpmulg  44154  relexp01min  44157  relexpxpmin  44161  unirnmap  45653  unirnmapsn  45659  ssmapsn  45661  fourierdlem70  46619  fourierdlem71  46620  fourierdlem80  46629  meadjiunlem  46908  omeiunle  46960  fexafv2ex  47683