Theorem rnexg 7854

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 7695	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7695	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun2 4133	. . . 4 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5931	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3945	. . 3 ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5270	. . 3 ⊢ ((ran 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → ran 𝐴 ∈ V)
7	5, 6	mpan 691	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → ran 𝐴 ∈ V)
8	1, 2, 7	3syl 18	1 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2114  Vcvv 3442   ∪ cun 3901   ⊆ wss 3903  ∪ cuni 4865  dom cdm 5632  ran crn 5633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-cnv 5640  df-dm 5642  df-rn 5643

This theorem is referenced by:  rnex  7862  imaexg  7865  rnexd  7867  xpexr  7870  xpexr2  7871  soex  7873  cnvexg  7876  coexg  7881  cofunexg  7903  funrnex  7908  tposexg  8192  iunon  8281  onoviun  8285  tz7.44lem1  8346  tz7.44-3  8349  fopwdom  9025  disjen  9074  domss2  9076  domssex  9078  hartogslem2  9460  ttrclexg  9644  djuexb  9833  dfac12lem2  10067  unirnfdomd  10490  hashimarn  14375  trclexlem  14929  relexp0g  14957  relexpsucnnr  14960  restval  17358  prdsbas  17389  prdsplusg  17390  prdsmulr  17391  prdsvsca  17392  prdshom  17399  sscpwex  17751  sylow1lem4  19542  sylow3lem2  19569  sylow3lem3  19570  lsmvalx  19580  txindislem  23589  xkoptsub  23610  fmfnfmlem3  23912  fmfnfmlem4  23913  ustuqtoplem  24195  ustuqtop0  24196  utopsnneiplem  24203  efabl  26527  efsubm  26528  addsuniflem  28009  sltmuls1  28155  sltmuls2  28156  precsexlem11  28225  perpln1  28794  perpln2  28795  isperp  28796  lmif  28869  islmib  28871  isgrpo  30585  grpoinvfval  30610  grpodivfval  30622  isvcOLD  30667  isnv  30700  abrexexd  32596  acunirnmpt  32749  acunirnmpt2  32750  acunirnmpt2f  32751  fnpreimac  32760  locfinreflem  34018  esumrnmpt2  34246  sxsigon  34370  omssubadd  34478  carsgclctunlem2  34497  pmeasadd  34503  sitgclg  34520  bnj1366  35005  ptrest  37870  elghomlem1OLD  38136  elghomlem2OLD  38137  isrngod  38149  iscringd  38249  xrnresex  38680  dfcnvrefrels2  38859  dfcnvrefrels3  38860  eldisjs7  39192  sticksstones3  42518  lmhmlnmsplit  43444  rclexi  43971  rtrclexlem  43972  trclubgNEW  43974  cnvrcl0  43981  dfrtrcl5  43985  relexpmulg  44066  relexp01min  44069  relexpxpmin  44073  unirnmap  45566  unirnmapsn  45572  ssmapsn  45574  fourierdlem70  46534  fourierdlem71  46535  fourierdlem80  46544  meadjiunlem  46823  omeiunle  46875  fexafv2ex  47580