Theorem rnexg 7881

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 7719	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7719	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun2 4145	. . . 4 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5940	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3959	. . 3 ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5281	. . 3 ⊢ ((ran 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → ran 𝐴 ∈ V)
7	5, 6	mpan 690	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → ran 𝐴 ∈ V)
8	1, 2, 7	3syl 18	1 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2109  Vcvv 3450   ∪ cun 3915   ⊆ wss 3917  ∪ cuni 4874  dom cdm 5641  ran crn 5642

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-cnv 5649  df-dm 5651  df-rn 5652

This theorem is referenced by:  rnex  7889  imaexg  7892  rnexd  7894  xpexr  7897  xpexr2  7898  soex  7900  cnvexg  7903  coexg  7908  cofunexg  7930  funrnex  7935  abrexexgOLD  7943  tposexg  8222  iunon  8311  onoviun  8315  tz7.44lem1  8376  tz7.44-3  8379  fopwdom  9054  disjen  9104  domss2  9106  domssex  9108  hartogslem2  9503  ttrclexg  9683  djuexb  9869  dfac12lem2  10105  unirnfdomd  10527  hashimarn  14412  trclexlem  14967  relexp0g  14995  relexpsucnnr  14998  restval  17396  prdsbas  17427  prdsplusg  17428  prdsmulr  17429  prdsvsca  17430  prdshom  17437  sscpwex  17784  sylow1lem4  19538  sylow3lem2  19565  sylow3lem3  19566  lsmvalx  19576  txindislem  23527  xkoptsub  23548  fmfnfmlem3  23850  fmfnfmlem4  23851  ustuqtoplem  24134  ustuqtop0  24135  utopsnneiplem  24142  efabl  26466  efsubm  26467  addsuniflem  27915  ssltmul1  28057  ssltmul2  28058  precsexlem11  28126  perpln1  28644  perpln2  28645  isperp  28646  lmif  28719  islmib  28721  isgrpo  30433  grpoinvfval  30458  grpodivfval  30470  isvcOLD  30515  isnv  30548  abrexexd  32445  acunirnmpt  32590  acunirnmpt2  32591  acunirnmpt2f  32592  fnpreimac  32602  locfinreflem  33837  esumrnmpt2  34065  sxsigon  34189  omssubadd  34298  carsgclctunlem2  34317  pmeasadd  34323  sitgclg  34340  bnj1366  34826  ptrest  37620  elghomlem1OLD  37886  elghomlem2OLD  37887  isrngod  37899  iscringd  37999  xrnresex  38399  dfcnvrefrels2  38526  dfcnvrefrels3  38527  sticksstones3  42143  lmhmlnmsplit  43083  rclexi  43611  rtrclexlem  43612  trclubgNEW  43614  cnvrcl0  43621  dfrtrcl5  43625  relexpmulg  43706  relexp01min  43709  relexpxpmin  43713  unirnmap  45209  unirnmapsn  45215  ssmapsn  45217  fourierdlem70  46181  fourierdlem71  46182  fourierdlem80  46191  meadjiunlem  46470  omeiunle  46522  fexafv2ex  47225