Theorem rnexg 7895

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 7730	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7730	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun2 4174	. . . 4 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5970	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3992	. . 3 ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5324	. . 3 ⊢ ((ran 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → ran 𝐴 ∈ V)
7	5, 6	mpan 689	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → ran 𝐴 ∈ V)
8	1, 2, 7	3syl 18	1 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2107  Vcvv 3475   ∪ cun 3947   ⊆ wss 3949  ∪ cuni 4909  dom cdm 5677  ran crn 5678

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7725

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-cnv 5685  df-dm 5687  df-rn 5688

This theorem is referenced by:  rnex  7903  imaexg  7906  xpexr  7909  xpexr2  7910  soex  7912  cnvexg  7915  coexg  7920  cofunexg  7935  funrnex  7940  abrexexgOLD  7948  tposexg  8225  iunon  8339  onoviun  8343  tz7.44lem1  8405  tz7.44-3  8408  fopwdom  9080  disjen  9134  domss2  9136  domssex  9138  hartogslem2  9538  ttrclexg  9718  djuexb  9904  dfac12lem2  10139  unirnfdomd  10562  hashimarn  14400  trclexlem  14941  relexp0g  14969  relexpsucnnr  14972  restval  17372  prdsbas  17403  prdsplusg  17404  prdsmulr  17405  prdsvsca  17406  prdshom  17413  sscpwex  17762  sylow1lem4  19469  sylow3lem2  19496  sylow3lem3  19497  lsmvalx  19507  txindislem  23137  xkoptsub  23158  fmfnfmlem3  23460  fmfnfmlem4  23461  ustuqtoplem  23744  ustuqtop0  23745  utopsnneiplem  23752  efabl  26059  efsubm  26060  addsuniflem  27484  ssltmul1  27602  ssltmul2  27603  precsexlem11  27663  perpln1  27961  perpln2  27962  isperp  27963  lmif  28036  islmib  28038  isgrpo  29750  grpoinvfval  29775  grpodivfval  29787  isvcOLD  29832  isnv  29865  abrexexd  31746  acunirnmpt  31884  acunirnmpt2  31885  acunirnmpt2f  31886  fnpreimac  31896  rnexd  31903  locfinreflem  32820  esumrnmpt2  33066  sxsigon  33190  omssubadd  33299  carsgclctunlem2  33318  pmeasadd  33324  sitgclg  33341  bnj1366  33840  ptrest  36487  elghomlem1OLD  36753  elghomlem2OLD  36754  isrngod  36766  iscringd  36866  imaexALTV  37199  xrnresex  37276  dfcnvrefrels2  37398  dfcnvrefrels3  37399  sticksstones3  40964  lmhmlnmsplit  41829  rclexi  42366  rtrclexlem  42367  trclubgNEW  42369  cnvrcl0  42376  dfrtrcl5  42380  relexpmulg  42461  relexp01min  42464  relexpxpmin  42468  unirnmap  43907  unirnmapsn  43913  ssmapsn  43915  fourierdlem70  44892  fourierdlem71  44893  fourierdlem80  44902  meadjiunlem  45181  omeiunle  45233  fexafv2ex  45928