Theorem rnexg 7745

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 7587	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7587	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun2 4112	. . . 4 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5878	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3935	. . 3 ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5251	. . 3 ⊢ ((ran 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → ran 𝐴 ∈ V)
7	5, 6	mpan 687	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → ran 𝐴 ∈ V)
8	1, 2, 7	3syl 18	1 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2110  Vcvv 3431   ∪ cun 3890   ⊆ wss 3892  ∪ cuni 4845  dom cdm 5590  ran crn 5591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356  ax-un 7582

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-br 5080  df-opab 5142  df-cnv 5598  df-dm 5600  df-rn 5601

This theorem is referenced by:  rnex  7753  imaexg  7756  xpexr  7759  xpexr2  7760  soex  7762  cnvexg  7765  coexg  7770  cofunexg  7785  funrnex  7790  abrexexg  7797  tposexg  8047  iunon  8161  onoviun  8165  tz7.44lem1  8227  tz7.44-3  8230  fopwdom  8849  disjen  8903  domss2  8905  domssex  8907  hartogslem2  9280  ttrclexg  9459  djuexb  9668  dfac12lem2  9901  unirnfdomd  10324  focdmex  14063  hashimarn  14153  trclexlem  14703  relexp0g  14731  relexpsucnnr  14734  restval  17135  prdsbas  17166  prdsplusg  17167  prdsmulr  17168  prdsvsca  17169  prdshom  17176  sscpwex  17525  sylow1lem4  19204  sylow3lem2  19231  sylow3lem3  19232  lsmvalx  19242  txindislem  22782  xkoptsub  22803  fmfnfmlem3  23105  fmfnfmlem4  23106  ustuqtoplem  23389  ustuqtop0  23390  utopsnneiplem  23397  efabl  25704  efsubm  25705  perpln1  27069  perpln2  27070  isperp  27071  lmif  27144  islmib  27146  isgrpo  28855  grpoinvfval  28880  grpodivfval  28892  isvcOLD  28937  isnv  28970  abrexexd  30850  acunirnmpt  30992  acunirnmpt2  30993  acunirnmpt2f  30994  fnpreimac  31004  locfinreflem  31786  esumrnmpt2  32032  sxsigon  32156  omssubadd  32263  carsgclctunlem2  32282  pmeasadd  32288  sitgclg  32305  bnj1366  32805  ptrest  35772  elghomlem1OLD  36039  elghomlem2OLD  36040  isrngod  36052  iscringd  36152  imaexALTV  36461  xrnresex  36528  dfcnvrefrels2  36640  dfcnvrefrels3  36641  sticksstones3  40101  lmhmlnmsplit  40909  rclexi  41193  rtrclexlem  41194  trclubgNEW  41196  cnvrcl0  41203  dfrtrcl5  41207  relexpmulg  41288  relexp01min  41291  relexpxpmin  41295  unirnmap  42718  unirnmapsn  42724  ssmapsn  42726  fourierdlem70  43688  fourierdlem71  43689  fourierdlem80  43698  meadjiunlem  43974  omeiunle  44026  fexafv2ex  44680