Theorem rnexg 7898

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 7738	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7738	. 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  7906  imaexg  7909  rnexd  7911  xpexr  7914  xpexr2  7915  soex  7917  cnvexg  7920  coexg  7925  cofunexg  7945  funrnex  7950  tposexg  8235  iunon  8325  onoviun  8329  tz7.44lem1  8391  tz7.44-3  8394  fopwdom  9072  disjen  9121  domss2  9123  domssex  9125  hartogslem2  9504  ttrclexg  9691  djuexb  9894  dfac12lem2  10127  unirnfdomd  10551  hashimarn  14476  trclexlem  15030  relexp0g  15058  relexpsucnnr  15061  restval  17478  prdsbas  17509  prdsplusg  17510  prdsmulr  17511  prdsvsca  17512  prdshom  17519  sscpwex  17871  sylow1lem4  19670  sylow3lem2  19697  sylow3lem3  19698  lsmvalx  19708  txindislem  23758  xkoptsub  23779  fmfnfmlem3  24081  fmfnfmlem4  24082  ustuqtoplem  24364  ustuqtop0  24365  utopsnneiplem  24372  efabl  26680  efsubm  26681  addsuniflem  28159  sltmuls1  28305  sltmuls2  28306  precsexlem11  28375  perpln1  28948  perpln2  28949  isperp  28950  lmif  29051  islmib  29053  isgrpo  30789  grpoinvfval  30814  grpodivfval  30826  isvcOLD  30871  isnv  30904  abrexexd  32795  acunirnmpt  32944  acunirnmpt2  32945  acunirnmpt2f  32946  fnpreimac  32955  locfinreflem  34174  esumrnmpt2  34402  sxsigon  34526  omssubadd  34634  carsgclctunlem2  34653  pmeasadd  34659  sitgclg  34676  bnj1366  35161  ptrest  38157  elghomlem1OLD  38423  elghomlem2OLD  38424  isrngod  38436  iscringd  38536  xrnresex  38967  dfcnvrefrels2  39146  dfcnvrefrels3  39147  eldisjs7  39479  sticksstones3  42804  lmhmlnmsplit  43705  rclexi  44232  rtrclexlem  44233  trclubgNEW  44235  cnvrcl0  44242  dfrtrcl5  44246  relexpmulg  44327  relexp01min  44330  relexpxpmin  44334  unirnmap  45815  unirnmapsn  45821  ssmapsn  45823  fourierdlem70  46781  fourierdlem71  46782  fourierdlem80  46791  meadjiunlem  47070  omeiunle  47122  fexafv2ex  47845