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  17757  sylow1lem4  19515  sylow3lem2  19542  sylow3lem3  19543  lsmvalx  19553  txindislem  23553  xkoptsub  23574  fmfnfmlem3  23876  fmfnfmlem4  23877  ustuqtoplem  24160  ustuqtop0  24161  utopsnneiplem  24168  efabl  26492  efsubm  26493  addsuniflem  27948  ssltmul1  28090  ssltmul2  28091  precsexlem11  28159  perpln1  28690  perpln2  28691  isperp  28692  lmif  28765  islmib  28767  isgrpo  30476  grpoinvfval  30501  grpodivfval  30513  isvcOLD  30558  isnv  30591  abrexexd  32488  acunirnmpt  32633  acunirnmpt2  32634  acunirnmpt2f  32635  fnpreimac  32645  locfinreflem  33823  esumrnmpt2  34051  sxsigon  34175  omssubadd  34284  carsgclctunlem2  34303  pmeasadd  34309  sitgclg  34326  bnj1366  34812  ptrest  37606  elghomlem1OLD  37872  elghomlem2OLD  37873  isrngod  37885  iscringd  37985  xrnresex  38385  dfcnvrefrels2  38512  dfcnvrefrels3  38513  sticksstones3  42129  lmhmlnmsplit  43069  rclexi  43597  rtrclexlem  43598  trclubgNEW  43600  cnvrcl0  43607  dfrtrcl5  43611  relexpmulg  43692  relexp01min  43695  relexpxpmin  43699  unirnmap  45195  unirnmapsn  45201  ssmapsn  45203  fourierdlem70  46167  fourierdlem71  46168  fourierdlem80  46177  meadjiunlem  46456  omeiunle  46508  fexafv2ex  47214