Theorem rnexg 7924

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 7760	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7760	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun2 4179	. . . 4 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5984	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3993	. . 3 ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5323	. . 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 2108  Vcvv 3480   ∪ cun 3949   ⊆ wss 3951  ∪ cuni 4907  dom cdm 5685  ran crn 5686

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-cnv 5693  df-dm 5695  df-rn 5696

This theorem is referenced by:  rnex  7932  imaexg  7935  rnexd  7937  xpexr  7940  xpexr2  7941  soex  7943  cnvexg  7946  coexg  7951  cofunexg  7973  funrnex  7978  abrexexgOLD  7986  tposexg  8265  iunon  8379  onoviun  8383  tz7.44lem1  8445  tz7.44-3  8448  fopwdom  9120  disjen  9174  domss2  9176  domssex  9178  hartogslem2  9583  ttrclexg  9763  djuexb  9949  dfac12lem2  10185  unirnfdomd  10607  hashimarn  14479  trclexlem  15033  relexp0g  15061  relexpsucnnr  15064  restval  17471  prdsbas  17502  prdsplusg  17503  prdsmulr  17504  prdsvsca  17505  prdshom  17512  sscpwex  17859  sylow1lem4  19619  sylow3lem2  19646  sylow3lem3  19647  lsmvalx  19657  txindislem  23641  xkoptsub  23662  fmfnfmlem3  23964  fmfnfmlem4  23965  ustuqtoplem  24248  ustuqtop0  24249  utopsnneiplem  24256  efabl  26592  efsubm  26593  addsuniflem  28034  ssltmul1  28173  ssltmul2  28174  precsexlem11  28241  perpln1  28718  perpln2  28719  isperp  28720  lmif  28793  islmib  28795  isgrpo  30516  grpoinvfval  30541  grpodivfval  30553  isvcOLD  30598  isnv  30631  abrexexd  32528  acunirnmpt  32669  acunirnmpt2  32670  acunirnmpt2f  32671  fnpreimac  32681  locfinreflem  33839  esumrnmpt2  34069  sxsigon  34193  omssubadd  34302  carsgclctunlem2  34321  pmeasadd  34327  sitgclg  34344  bnj1366  34843  ptrest  37626  elghomlem1OLD  37892  elghomlem2OLD  37893  isrngod  37905  iscringd  38005  imaexALTV  38331  xrnresex  38407  dfcnvrefrels2  38529  dfcnvrefrels3  38530  sticksstones3  42149  lmhmlnmsplit  43099  rclexi  43628  rtrclexlem  43629  trclubgNEW  43631  cnvrcl0  43638  dfrtrcl5  43642  relexpmulg  43723  relexp01min  43726  relexpxpmin  43730  unirnmap  45213  unirnmapsn  45219  ssmapsn  45221  fourierdlem70  46191  fourierdlem71  46192  fourierdlem80  46201  meadjiunlem  46480  omeiunle  46532  fexafv2ex  47232