Theorem rnexg 7858

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 7696	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7696	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun2 4138	. . . 4 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5926	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3953	. . 3 ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5273	. . 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 2109  Vcvv 3444   ∪ cun 3909   ⊆ wss 3911  ∪ cuni 4867  dom cdm 5631  ran crn 5632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382  ax-un 7691

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-cnv 5639  df-dm 5641  df-rn 5642

This theorem is referenced by:  rnex  7866  imaexg  7869  rnexd  7871  xpexr  7874  xpexr2  7875  soex  7877  cnvexg  7880  coexg  7885  cofunexg  7907  funrnex  7912  tposexg  8196  iunon  8285  onoviun  8289  tz7.44lem1  8350  tz7.44-3  8353  fopwdom  9026  disjen  9075  domss2  9077  domssex  9079  hartogslem2  9472  ttrclexg  9652  djuexb  9838  dfac12lem2  10074  unirnfdomd  10496  hashimarn  14381  trclexlem  14936  relexp0g  14964  relexpsucnnr  14967  restval  17365  prdsbas  17396  prdsplusg  17397  prdsmulr  17398  prdsvsca  17399  prdshom  17406  sscpwex  17753  sylow1lem4  19507  sylow3lem2  19534  sylow3lem3  19535  lsmvalx  19545  txindislem  23496  xkoptsub  23517  fmfnfmlem3  23819  fmfnfmlem4  23820  ustuqtoplem  24103  ustuqtop0  24104  utopsnneiplem  24111  efabl  26435  efsubm  26436  addsuniflem  27884  ssltmul1  28026  ssltmul2  28027  precsexlem11  28095  perpln1  28613  perpln2  28614  isperp  28615  lmif  28688  islmib  28690  isgrpo  30399  grpoinvfval  30424  grpodivfval  30436  isvcOLD  30481  isnv  30514  abrexexd  32411  acunirnmpt  32556  acunirnmpt2  32557  acunirnmpt2f  32558  fnpreimac  32568  locfinreflem  33803  esumrnmpt2  34031  sxsigon  34155  omssubadd  34264  carsgclctunlem2  34283  pmeasadd  34289  sitgclg  34306  bnj1366  34792  ptrest  37586  elghomlem1OLD  37852  elghomlem2OLD  37853  isrngod  37865  iscringd  37965  xrnresex  38365  dfcnvrefrels2  38492  dfcnvrefrels3  38493  sticksstones3  42109  lmhmlnmsplit  43049  rclexi  43577  rtrclexlem  43578  trclubgNEW  43580  cnvrcl0  43587  dfrtrcl5  43591  relexpmulg  43672  relexp01min  43675  relexpxpmin  43679  unirnmap  45175  unirnmapsn  45181  ssmapsn  45183  fourierdlem70  46147  fourierdlem71  46148  fourierdlem80  46157  meadjiunlem  46436  omeiunle  46488  fexafv2ex  47194