Theorem rnexg 7914

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 7757	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7757	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun2 4125	. . . 4 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5956	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3940	. . 3 ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5281	. . 3 ⊢ ((ran 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → ran 𝐴 ∈ V)
7	5, 6	mpan 703	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → ran 𝐴 ∈ V)
8	1, 2, 7	3syl 19	1 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3451   ∪ cun 3897   ⊆ wss 3899  ∪ cuni 4867  dom cdm 5651  ran crn 5652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-cnv 5659  df-dm 5661  df-rn 5662

This theorem is used by:  rnex  7922  imaexg  7925  rnexd  7927  xpexr  7930  xpexr2  7931  soex  7933  cnvexg  7936  coexg  7941  cofunexg  7961  funrnex  7966  tposexg  8257  iunon  8347  onoviun  8351  tz7.44lem1  8413  tz7.44-3  8416  fopwdom  9104  disjen  9153  domss2  9155  domssex  9157  hartogslem2  9537  ttrclexg  9724  djuexb  9990  dfac12lem2  10223  unirnfdomd  10652  hashimarn  14585  trclexlem  15147  relexp0g  15175  relexpsucnnr  15178  restval  17597  prdsbas  17628  prdsplusg  17629  prdsmulr  17630  prdsvsca  17631  prdshom  17638  sscpwex  17990  sylow1lem4  19815  sylow3lem2  19842  sylow3lem3  19843  lsmvalx  19853  txindislem  23952  xkoptsub  23973  fmfnfmlem3  24275  fmfnfmlem4  24276  ustuqtoplem  24558  ustuqtop0  24559  utopsnneiplem  24566  efabl  26878  efsubm  26879  addsuniflem  28387  sltmuls1  28533  sltmuls2  28534  precsexlem11  28603  perpln1  29185  perpln2  29186  isperp  29187  lmif  29290  islmib  29292  isgrpo  31099  grpoinvfval  31124  grpodivfval  31136  isvcOLD  31181  isnv  31214  abrexexd  33105  acunirnmpt  33253  acunirnmpt2  33254  acunirnmpt2f  33255  fnpreimac  33264  locfinreflem  34472  esumrnmpt2  34700  sxsigon  34825  omssubadd  34932  carsgclctunlem2  34951  pmeasadd  34957  sitgclg  34974  bnj1366  35459  ptrest  38537  elghomlem1OLD  38819  elghomlem2OLD  38820  isrngod  38832  iscringd  38932  xrnresex  39361  dfcnvrefrels2  39540  dfcnvrefrels3  39541  eldisjs7  39873  sticksstones3  43198  lmhmlnmsplit  44088  rclexi  44614  rtrclexlem  44615  trclubgNEW  44617  cnvrcl0  44624  dfrtrcl5  44628  relexpmulg  44709  relexp01min  44712  relexpxpmin  44716  unirnmap  46220  unirnmapsn  46226  ssmapsn  46228  fourierdlem70  47185  fourierdlem71  47186  fourierdlem80  47195  meadjiunlem  47474  omeiunle  47526  fexafv2ex  48289