Theorem rnexg 7844

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 7685	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7685	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun2 4131	. . . 4 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5923	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3943	. . 3 ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5268	. . 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 2113  Vcvv 3440   ∪ cun 3899   ⊆ wss 3901  ∪ cuni 4863  dom cdm 5624  ran crn 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-cnv 5632  df-dm 5634  df-rn 5635

This theorem is referenced by:  rnex  7852  imaexg  7855  rnexd  7857  xpexr  7860  xpexr2  7861  soex  7863  cnvexg  7866  coexg  7871  cofunexg  7893  funrnex  7898  tposexg  8182  iunon  8271  onoviun  8275  tz7.44lem1  8336  tz7.44-3  8339  fopwdom  9013  disjen  9062  domss2  9064  domssex  9066  hartogslem2  9448  ttrclexg  9632  djuexb  9821  dfac12lem2  10055  unirnfdomd  10478  hashimarn  14363  trclexlem  14917  relexp0g  14945  relexpsucnnr  14948  restval  17346  prdsbas  17377  prdsplusg  17378  prdsmulr  17379  prdsvsca  17380  prdshom  17387  sscpwex  17739  sylow1lem4  19530  sylow3lem2  19557  sylow3lem3  19558  lsmvalx  19568  txindislem  23577  xkoptsub  23598  fmfnfmlem3  23900  fmfnfmlem4  23901  ustuqtoplem  24183  ustuqtop0  24184  utopsnneiplem  24191  efabl  26515  efsubm  26516  addsuniflem  27997  sltmuls1  28143  sltmuls2  28144  precsexlem11  28213  perpln1  28782  perpln2  28783  isperp  28784  lmif  28857  islmib  28859  isgrpo  30572  grpoinvfval  30597  grpodivfval  30609  isvcOLD  30654  isnv  30687  abrexexd  32584  acunirnmpt  32737  acunirnmpt2  32738  acunirnmpt2f  32739  fnpreimac  32749  locfinreflem  33997  esumrnmpt2  34225  sxsigon  34349  omssubadd  34457  carsgclctunlem2  34476  pmeasadd  34482  sitgclg  34499  bnj1366  34985  ptrest  37820  elghomlem1OLD  38086  elghomlem2OLD  38087  isrngod  38099  iscringd  38199  xrnresex  38614  dfcnvrefrels2  38781  dfcnvrefrels3  38782  sticksstones3  42402  lmhmlnmsplit  43329  rclexi  43856  rtrclexlem  43857  trclubgNEW  43859  cnvrcl0  43866  dfrtrcl5  43870  relexpmulg  43951  relexp01min  43954  relexpxpmin  43958  unirnmap  45452  unirnmapsn  45458  ssmapsn  45460  fourierdlem70  46420  fourierdlem71  46421  fourierdlem80  46430  meadjiunlem  46709  omeiunle  46761  fexafv2ex  47466