Theorem rnexg 7243

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 7100	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7100	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun2 3928	. . . 4 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5520	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3761	. . 3 ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 4938	. . 3 ⊢ ((ran 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → ran 𝐴 ∈ V)
7	5, 6	mpan 670	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → ran 𝐴 ∈ V)
8	1, 2, 7	3syl 18	1 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2145  Vcvv 3351   ∪ cun 3721   ⊆ wss 3723  ∪ cuni 4574  dom cdm 5249  ran crn 5250

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pr 5034  ax-un 7094

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rex 3067  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-cnv 5257  df-dm 5259  df-rn 5260

This theorem is referenced by:  rnex  7245  imaexg  7248  xpexr  7251  xpexr2  7252  soex  7254  cnvexg  7257  coexg  7262  cofunexg  7275  funrnex  7278  abrexexg  7285  tposexg  7516  iunon  7587  onoviun  7591  tz7.44lem1  7652  tz7.44-3  7655  fopwdom  8222  disjen  8271  domss2  8273  domssex  8275  hartogslem2  8602  dfac12lem2  9166  unirnfdomd  9589  focdmex  13336  hashimarn  13422  trclexlem  13936  relexp0g  13963  relexpsucnnr  13966  restval  16288  prdsbas  16318  prdsplusg  16319  prdsmulr  16320  prdsvsca  16321  prdshom  16328  sscpwex  16675  sylow1lem4  18216  sylow3lem2  18243  sylow3lem3  18244  lsmvalx  18254  txindislem  21650  xkoptsub  21671  fmfnfmlem3  21973  fmfnfmlem4  21974  ustuqtoplem  22256  ustuqtop0  22257  utopsnneiplem  22264  efabl  24510  efsubm  24511  perpln1  25819  perpln2  25820  isperp  25821  lmif  25891  islmib  25893  isgrpo  27684  grpoinvfval  27709  grpodivfval  27721  isvcOLD  27767  isnv  27800  abrexexd  29678  acunirnmpt  29792  acunirnmpt2  29793  acunirnmpt2f  29794  locfinreflem  30240  esumrnmpt2  30463  sxsigon  30588  omssubadd  30695  carsgclctunlem2  30714  pmeasadd  30720  sitgclg  30737  bnj1366  31231  ptrest  33734  elghomlem1OLD  34009  elghomlem2OLD  34010  isrngod  34022  iscringd  34122  xrnresex  34499  dfcnvrefrels2  34611  dfcnvrefrels3  34612  lmhmlnmsplit  38176  rclexi  38441  rtrclexlem  38442  trclubgNEW  38444  cnvrcl0  38451  dfrtrcl5  38455  relexpmulg  38521  relexp01min  38524  relexpxpmin  38528  unirnmap  39911  unirnmapsn  39917  ssmapsn  39919  fourierdlem70  40903  fourierdlem71  40904  fourierdlem80  40913  meadjiunlem  41192  omeiunle  41244