Theorem rnexg 7835

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 7676	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7676	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun2 4130	. . . 4 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5915	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3945	. . 3 ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5262	. . 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 3436   ∪ cun 3901   ⊆ wss 3903  ∪ cuni 4858  dom cdm 5619  ran crn 5620

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 5235  ax-nul 5245  ax-pr 5371  ax-un 7671

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 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-cnv 5627  df-dm 5629  df-rn 5630

This theorem is referenced by:  rnex  7843  imaexg  7846  rnexd  7848  xpexr  7851  xpexr2  7852  soex  7854  cnvexg  7857  coexg  7862  cofunexg  7884  funrnex  7889  tposexg  8173  iunon  8262  onoviun  8266  tz7.44lem1  8327  tz7.44-3  8330  fopwdom  9002  disjen  9051  domss2  9053  domssex  9055  hartogslem2  9435  ttrclexg  9619  djuexb  9805  dfac12lem2  10039  unirnfdomd  10461  hashimarn  14347  trclexlem  14901  relexp0g  14929  relexpsucnnr  14932  restval  17330  prdsbas  17361  prdsplusg  17362  prdsmulr  17363  prdsvsca  17364  prdshom  17371  sscpwex  17722  sylow1lem4  19480  sylow3lem2  19507  sylow3lem3  19508  lsmvalx  19518  txindislem  23518  xkoptsub  23539  fmfnfmlem3  23841  fmfnfmlem4  23842  ustuqtoplem  24125  ustuqtop0  24126  utopsnneiplem  24133  efabl  26457  efsubm  26458  addsuniflem  27913  ssltmul1  28055  ssltmul2  28056  precsexlem11  28124  perpln1  28655  perpln2  28656  isperp  28657  lmif  28730  islmib  28732  isgrpo  30441  grpoinvfval  30466  grpodivfval  30478  isvcOLD  30523  isnv  30556  abrexexd  32453  acunirnmpt  32602  acunirnmpt2  32603  acunirnmpt2f  32604  fnpreimac  32614  locfinreflem  33807  esumrnmpt2  34035  sxsigon  34159  omssubadd  34268  carsgclctunlem2  34287  pmeasadd  34293  sitgclg  34310  bnj1366  34796  ptrest  37603  elghomlem1OLD  37869  elghomlem2OLD  37870  isrngod  37882  iscringd  37982  xrnresex  38382  dfcnvrefrels2  38509  dfcnvrefrels3  38510  sticksstones3  42125  lmhmlnmsplit  43064  rclexi  43592  rtrclexlem  43593  trclubgNEW  43595  cnvrcl0  43602  dfrtrcl5  43606  relexpmulg  43687  relexp01min  43690  relexpxpmin  43694  unirnmap  45190  unirnmapsn  45196  ssmapsn  45198  fourierdlem70  46161  fourierdlem71  46162  fourierdlem80  46171  meadjiunlem  46450  omeiunle  46502  fexafv2ex  47208