Theorem rnexg 7900

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 7743	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7743	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun2 4125	. . . 4 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5958	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3940	. . 3 ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5284	. . 3 ⊢ ((ran 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → ran 𝐴 ∈ V)
7	5, 6	mpan 703	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → ran 𝐴 ∈ V)
8	1, 2, 7	3syl 19	1 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  Vcvv 3450   ∪ cun 3897   ⊆ wss 3899  ∪ cuni 4867  dom cdm 5655  ran crn 5656

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pr 5398  ax-un 7737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-cnv 5663  df-dm 5665  df-rn 5666

This theorem is used by:  rnex  7908  imaexg  7911  rnexd  7913  xpexr  7916  xpexr2  7917  soex  7919  cnvexg  7922  coexg  7927  cofunexg  7947  funrnex  7952  tposexg  8239  iunon  8329  onoviun  8333  tz7.44lem1  8395  tz7.44-3  8398  fopwdom  9084  disjen  9133  domss2  9135  domssex  9137  hartogslem2  9516  ttrclexg  9703  djuexb  9915  dfac12lem2  10148  unirnfdomd  10577  hashimarn  14506  trclexlem  15068  relexp0g  15096  relexpsucnnr  15099  restval  17512  prdsbas  17543  prdsplusg  17544  prdsmulr  17545  prdsvsca  17546  prdshom  17553  sscpwex  17905  sylow1lem4  19729  sylow3lem2  19756  sylow3lem3  19757  lsmvalx  19767  txindislem  23860  xkoptsub  23881  fmfnfmlem3  24183  fmfnfmlem4  24184  ustuqtoplem  24466  ustuqtop0  24467  utopsnneiplem  24474  efabl  26788  efsubm  26789  addsuniflem  28267  sltmuls1  28413  sltmuls2  28414  precsexlem11  28483  perpln1  29065  perpln2  29066  isperp  29067  lmif  29170  islmib  29172  isgrpo  30979  grpoinvfval  31004  grpodivfval  31016  isvcOLD  31061  isnv  31094  abrexexd  32985  acunirnmpt  33133  acunirnmpt2  33134  acunirnmpt2f  33135  fnpreimac  33144  locfinreflem  34351  esumrnmpt2  34579  sxsigon  34704  omssubadd  34812  carsgclctunlem2  34831  pmeasadd  34837  sitgclg  34854  bnj1366  35339  ptrest  38369  elghomlem1OLD  38636  elghomlem2OLD  38637  isrngod  38649  iscringd  38749  xrnresex  39178  dfcnvrefrels2  39357  dfcnvrefrels3  39358  eldisjs7  39690  sticksstones3  43015  lmhmlnmsplit  43929  rclexi  44456  rtrclexlem  44457  trclubgNEW  44459  cnvrcl0  44466  dfrtrcl5  44470  relexpmulg  44551  relexp01min  44554  relexpxpmin  44558  unirnmap  46039  unirnmapsn  46045  ssmapsn  46047  fourierdlem70  47005  fourierdlem71  47006  fourierdlem80  47015  meadjiunlem  47294  omeiunle  47346  fexafv2ex  48109