Theorem rnexg 7942

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 7775	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7775	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun2 4202	. . . 4 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5996	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 4018	. . 3 ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5341	. . 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 2108  Vcvv 3488   ∪ cun 3974   ⊆ wss 3976  ∪ cuni 4931  dom cdm 5700  ran crn 5701

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-cnv 5708  df-dm 5710  df-rn 5711

This theorem is referenced by:  rnex  7950  imaexg  7953  rnexd  7955  xpexr  7958  xpexr2  7959  soex  7961  cnvexg  7964  coexg  7969  cofunexg  7989  funrnex  7994  abrexexgOLD  8002  tposexg  8281  iunon  8395  onoviun  8399  tz7.44lem1  8461  tz7.44-3  8464  fopwdom  9146  disjen  9200  domss2  9202  domssex  9204  hartogslem2  9612  ttrclexg  9792  djuexb  9978  dfac12lem2  10214  unirnfdomd  10636  hashimarn  14489  trclexlem  15043  relexp0g  15071  relexpsucnnr  15074  restval  17486  prdsbas  17517  prdsplusg  17518  prdsmulr  17519  prdsvsca  17520  prdshom  17527  sscpwex  17876  sylow1lem4  19643  sylow3lem2  19670  sylow3lem3  19671  lsmvalx  19681  txindislem  23662  xkoptsub  23683  fmfnfmlem3  23985  fmfnfmlem4  23986  ustuqtoplem  24269  ustuqtop0  24270  utopsnneiplem  24277  efabl  26610  efsubm  26611  addsuniflem  28052  ssltmul1  28191  ssltmul2  28192  precsexlem11  28259  perpln1  28736  perpln2  28737  isperp  28738  lmif  28811  islmib  28813  isgrpo  30529  grpoinvfval  30554  grpodivfval  30566  isvcOLD  30611  isnv  30644  abrexexd  32537  acunirnmpt  32677  acunirnmpt2  32678  acunirnmpt2f  32679  fnpreimac  32689  locfinreflem  33786  esumrnmpt2  34032  sxsigon  34156  omssubadd  34265  carsgclctunlem2  34284  pmeasadd  34290  sitgclg  34307  bnj1366  34805  ptrest  37579  elghomlem1OLD  37845  elghomlem2OLD  37846  isrngod  37858  iscringd  37958  imaexALTV  38286  xrnresex  38362  dfcnvrefrels2  38484  dfcnvrefrels3  38485  sticksstones3  42105  lmhmlnmsplit  43044  rclexi  43577  rtrclexlem  43578  trclubgNEW  43580  cnvrcl0  43587  dfrtrcl5  43591  relexpmulg  43672  relexp01min  43675  relexpxpmin  43679  unirnmap  45115  unirnmapsn  45121  ssmapsn  45123  fourierdlem70  46097  fourierdlem71  46098  fourierdlem80  46107  meadjiunlem  46386  omeiunle  46438  fexafv2ex  47135