Theorem rnexg 7899

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 7739	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7739	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun2 4140	. . . 4 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5965	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3954	. . 3 ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5294	. . 3 ⊢ ((ran 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → ran 𝐴 ∈ V)
7	5, 6	mpan 702	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → ran 𝐴 ∈ V)
8	1, 2, 7	3syl 19	1 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2149  Vcvv 3463   ∪ cun 3911   ⊆ wss 3913  ∪ cuni 4876  dom cdm 5662  ran crn 5663

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5261  ax-pr 5405  ax-un 7733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-cnv 5670  df-dm 5672  df-rn 5673

This theorem is referenced by:  rnex  7907  imaexg  7910  rnexd  7912  xpexr  7915  xpexr2  7916  soex  7918  cnvexg  7921  coexg  7926  cofunexg  7946  funrnex  7951  tposexg  8236  iunon  8326  onoviun  8330  tz7.44lem1  8392  tz7.44-3  8395  fopwdom  9073  disjen  9122  domss2  9124  domssex  9126  hartogslem2  9505  ttrclexg  9692  djuexb  9895  dfac12lem2  10128  unirnfdomd  10552  hashimarn  14477  trclexlem  15031  relexp0g  15059  relexpsucnnr  15062  restval  17479  prdsbas  17510  prdsplusg  17511  prdsmulr  17512  prdsvsca  17513  prdshom  17520  sscpwex  17872  sylow1lem4  19671  sylow3lem2  19698  sylow3lem3  19699  lsmvalx  19709  txindislem  23759  xkoptsub  23780  fmfnfmlem3  24082  fmfnfmlem4  24083  ustuqtoplem  24365  ustuqtop0  24366  utopsnneiplem  24373  efabl  26681  efsubm  26682  addsuniflem  28160  sltmuls1  28306  sltmuls2  28307  precsexlem11  28376  perpln1  28949  perpln2  28950  isperp  28951  lmif  29052  islmib  29054  isgrpo  30790  grpoinvfval  30815  grpodivfval  30827  isvcOLD  30872  isnv  30905  abrexexd  32796  acunirnmpt  32945  acunirnmpt2  32946  acunirnmpt2f  32947  fnpreimac  32956  locfinreflem  34175  esumrnmpt2  34403  sxsigon  34527  omssubadd  34635  carsgclctunlem2  34654  pmeasadd  34660  sitgclg  34677  bnj1366  35162  ptrest  38158  elghomlem1OLD  38424  elghomlem2OLD  38425  isrngod  38437  iscringd  38537  xrnresex  38968  dfcnvrefrels2  39147  dfcnvrefrels3  39148  eldisjs7  39480  sticksstones3  42805  lmhmlnmsplit  43706  rclexi  44233  rtrclexlem  44234  trclubgNEW  44236  cnvrcl0  44243  dfrtrcl5  44247  relexpmulg  44328  relexp01min  44331  relexpxpmin  44335  unirnmap  45816  unirnmapsn  45822  ssmapsn  45824  fourierdlem70  46782  fourierdlem71  46783  fourierdlem80  46792  meadjiunlem  47071  omeiunle  47123  fexafv2ex  47846