Theorem rnexg 7905

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 7748	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7748	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun2 4132	. . . 4 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5966	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3947	. . 3 ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5292	. . 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 2146  Vcvv 3457   ∪ cun 3904   ⊆ wss 3906  ∪ cuni 4874  dom cdm 5663  ran crn 5664

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 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406  ax-un 7742

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 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-cnv 5671  df-dm 5673  df-rn 5674

This theorem is used by:  rnex  7913  imaexg  7916  rnexd  7918  xpexr  7921  xpexr2  7922  soex  7924  cnvexg  7927  coexg  7932  cofunexg  7952  funrnex  7957  tposexg  8242  iunon  8332  onoviun  8336  tz7.44lem1  8398  tz7.44-3  8401  fopwdom  9080  disjen  9129  domss2  9131  domssex  9133  hartogslem2  9512  ttrclexg  9699  djuexb  9911  dfac12lem2  10144  unirnfdomd  10569  hashimarn  14497  trclexlem  15057  relexp0g  15085  relexpsucnnr  15088  restval  17503  prdsbas  17534  prdsplusg  17535  prdsmulr  17536  prdsvsca  17537  prdshom  17544  sscpwex  17896  sylow1lem4  19717  sylow3lem2  19744  sylow3lem3  19745  lsmvalx  19755  txindislem  23843  xkoptsub  23864  fmfnfmlem3  24166  fmfnfmlem4  24167  ustuqtoplem  24449  ustuqtop0  24450  utopsnneiplem  24457  efabl  26768  efsubm  26769  addsuniflem  28247  sltmuls1  28393  sltmuls2  28394  precsexlem11  28463  perpln1  29043  perpln2  29044  isperp  29045  lmif  29147  islmib  29149  isgrpo  30922  grpoinvfval  30947  grpodivfval  30959  isvcOLD  31004  isnv  31037  abrexexd  32928  acunirnmpt  33077  acunirnmpt2  33078  acunirnmpt2f  33079  fnpreimac  33088  locfinreflem  34296  esumrnmpt2  34524  sxsigon  34649  omssubadd  34757  carsgclctunlem2  34776  pmeasadd  34782  sitgclg  34799  bnj1366  35284  ptrest  38329  elghomlem1OLD  38596  elghomlem2OLD  38597  isrngod  38609  iscringd  38709  xrnresex  39138  dfcnvrefrels2  39317  dfcnvrefrels3  39318  eldisjs7  39650  sticksstones3  42975  lmhmlnmsplit  43874  rclexi  44401  rtrclexlem  44402  trclubgNEW  44404  cnvrcl0  44411  dfrtrcl5  44415  relexpmulg  44496  relexp01min  44499  relexpxpmin  44503  unirnmap  45984  unirnmapsn  45990  ssmapsn  45992  fourierdlem70  46950  fourierdlem71  46951  fourierdlem80  46960  meadjiunlem  47239  omeiunle  47291  fexafv2ex  48017