Theorem rnexg 7883

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 7723	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7723	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun2 4131	. . . 4 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5950	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3945	. . 3 ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5279	. . 3 ⊢ ((ran 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → ran 𝐴 ∈ V)
7	5, 6	mpan 700	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → ran 𝐴 ∈ V)
8	1, 2, 7	3syl 18	1 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2142  Vcvv 3454   ∪ cun 3902   ⊆ wss 3904  ∪ cuni 4865  dom cdm 5647  ran crn 5648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-sep 5246  ax-pr 5390  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-cnv 5655  df-dm 5657  df-rn 5658

This theorem is referenced by:  rnex  7891  imaexg  7894  rnexd  7896  xpexr  7899  xpexr2  7900  soex  7902  cnvexg  7905  coexg  7910  cofunexg  7930  funrnex  7935  tposexg  8220  iunon  8310  onoviun  8314  tz7.44lem1  8376  tz7.44-3  8379  fopwdom  9057  disjen  9106  domss2  9108  domssex  9110  hartogslem2  9491  ttrclexg  9678  djuexb  9867  dfac12lem2  10101  unirnfdomd  10525  hashimarn  14453  trclexlem  15007  relexp0g  15035  relexpsucnnr  15038  restval  17455  prdsbas  17486  prdsplusg  17487  prdsmulr  17488  prdsvsca  17489  prdshom  17496  sscpwex  17848  sylow1lem4  19641  sylow3lem2  19668  sylow3lem3  19669  lsmvalx  19679  txindislem  23693  xkoptsub  23714  fmfnfmlem3  24016  fmfnfmlem4  24017  ustuqtoplem  24299  ustuqtop0  24300  utopsnneiplem  24307  efabl  26615  efsubm  26616  addsuniflem  28094  sltmuls1  28240  sltmuls2  28241  precsexlem11  28310  perpln1  28883  perpln2  28884  isperp  28885  lmif  28958  islmib  28960  isgrpo  30700  grpoinvfval  30725  grpodivfval  30737  isvcOLD  30782  isnv  30815  abrexexd  32708  acunirnmpt  32861  acunirnmpt2  32862  acunirnmpt2f  32863  fnpreimac  32872  locfinreflem  34137  esumrnmpt2  34365  sxsigon  34489  omssubadd  34597  carsgclctunlem2  34616  pmeasadd  34622  sitgclg  34639  bnj1366  35124  ptrest  38118  elghomlem1OLD  38384  elghomlem2OLD  38385  isrngod  38397  iscringd  38497  xrnresex  38928  dfcnvrefrels2  39107  dfcnvrefrels3  39108  eldisjs7  39440  sticksstones3  42765  lmhmlnmsplit  43664  rclexi  44191  rtrclexlem  44192  trclubgNEW  44194  cnvrcl0  44201  dfrtrcl5  44205  relexpmulg  44286  relexp01min  44289  relexpxpmin  44293  unirnmap  45784  unirnmapsn  45790  ssmapsn  45792  fourierdlem70  46750  fourierdlem71  46751  fourierdlem80  46760  meadjiunlem  47039  omeiunle  47091  fexafv2ex  47814