Theorem rnexg 7910

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 7746	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7746	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun2 4171	. . . 4 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5973	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3986	. . 3 ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5324	. . 3 ⊢ ((ran 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → ran 𝐴 ∈ V)
7	5, 6	mpan 688	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → ran 𝐴 ∈ V)
8	1, 2, 7	3syl 18	1 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2098  Vcvv 3461   ∪ cun 3942   ⊆ wss 3944  ∪ cuni 4909  dom cdm 5678  ran crn 5679

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696  ax-sep 5300  ax-nul 5307  ax-pr 5429  ax-un 7741

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-br 5150  df-opab 5212  df-cnv 5686  df-dm 5688  df-rn 5689

This theorem is referenced by:  rnex  7918  imaexg  7921  rnexd  7923  xpexr  7926  xpexr2  7927  soex  7929  cnvexg  7932  coexg  7937  cofunexg  7953  funrnex  7958  abrexexgOLD  7966  tposexg  8246  iunon  8360  onoviun  8364  tz7.44lem1  8426  tz7.44-3  8429  fopwdom  9105  disjen  9159  domss2  9161  domssex  9163  hartogslem2  9568  ttrclexg  9748  djuexb  9934  dfac12lem2  10169  unirnfdomd  10592  hashimarn  14435  trclexlem  14977  relexp0g  15005  relexpsucnnr  15008  restval  17411  prdsbas  17442  prdsplusg  17443  prdsmulr  17444  prdsvsca  17445  prdshom  17452  sscpwex  17801  sylow1lem4  19568  sylow3lem2  19595  sylow3lem3  19596  lsmvalx  19606  txindislem  23581  xkoptsub  23602  fmfnfmlem3  23904  fmfnfmlem4  23905  ustuqtoplem  24188  ustuqtop0  24189  utopsnneiplem  24196  efabl  26529  efsubm  26530  addsuniflem  27964  ssltmul1  28097  ssltmul2  28098  precsexlem11  28165  perpln1  28586  perpln2  28587  isperp  28588  lmif  28661  islmib  28663  isgrpo  30379  grpoinvfval  30404  grpodivfval  30416  isvcOLD  30461  isnv  30494  abrexexd  32382  acunirnmpt  32526  acunirnmpt2  32527  acunirnmpt2f  32528  fnpreimac  32538  locfinreflem  33572  esumrnmpt2  33818  sxsigon  33942  omssubadd  34051  carsgclctunlem2  34070  pmeasadd  34076  sitgclg  34093  bnj1366  34591  ptrest  37223  elghomlem1OLD  37489  elghomlem2OLD  37490  isrngod  37502  iscringd  37602  imaexALTV  37932  xrnresex  38008  dfcnvrefrels2  38130  dfcnvrefrels3  38131  sticksstones3  41751  lmhmlnmsplit  42653  rclexi  43187  rtrclexlem  43188  trclubgNEW  43190  cnvrcl0  43197  dfrtrcl5  43201  relexpmulg  43282  relexp01min  43285  relexpxpmin  43289  unirnmap  44720  unirnmapsn  44726  ssmapsn  44728  fourierdlem70  45702  fourierdlem71  45703  fourierdlem80  45712  meadjiunlem  45991  omeiunle  46043  fexafv2ex  46738