Theorem rnexg 7846

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 7682	. 2 ⊢ (𝐴 ∈ 𝑉 → ∪ 𝐴 ∈ V)
2		uniexg 7682	. 2 ⊢ (∪ 𝐴 ∈ V → ∪ ∪ 𝐴 ∈ V)
3		ssun2 4138	. . . 4 ⊢ ran 𝐴 ⊆ (dom 𝐴 ∪ ran 𝐴)
4		dmrnssfld 5930	. . . 4 ⊢ (dom 𝐴 ∪ ran 𝐴) ⊆ ∪ ∪ 𝐴
5	3, 4	sstri 3956	. . 3 ⊢ ran 𝐴 ⊆ ∪ ∪ 𝐴
6		ssexg 5285	. . 3 ⊢ ((ran 𝐴 ⊆ ∪ ∪ 𝐴 ∧ ∪ ∪ 𝐴 ∈ V) → ran 𝐴 ∈ V)
7	5, 6	mpan 688	. 2 ⊢ (∪ ∪ 𝐴 ∈ V → ran 𝐴 ∈ V)
8	1, 2, 7	3syl 18	1 ⊢ (𝐴 ∈ 𝑉 → ran 𝐴 ∈ V)

Syntax hints:   → wi 4   ∈ wcel 2106  Vcvv 3446   ∪ cun 3911   ⊆ wss 3913  ∪ cuni 4870  dom cdm 5638  ran crn 5639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389  ax-un 7677

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-cnv 5646  df-dm 5648  df-rn 5649

This theorem is referenced by:  rnex  7854  imaexg  7857  xpexr  7860  xpexr2  7861  soex  7863  cnvexg  7866  coexg  7871  cofunexg  7886  funrnex  7891  abrexexgOLD  7899  tposexg  8176  iunon  8290  onoviun  8294  tz7.44lem1  8356  tz7.44-3  8359  fopwdom  9031  disjen  9085  domss2  9087  domssex  9089  hartogslem2  9488  ttrclexg  9668  djuexb  9854  dfac12lem2  10089  unirnfdomd  10512  hashimarn  14350  trclexlem  14891  relexp0g  14919  relexpsucnnr  14922  restval  17322  prdsbas  17353  prdsplusg  17354  prdsmulr  17355  prdsvsca  17356  prdshom  17363  sscpwex  17712  sylow1lem4  19397  sylow3lem2  19424  sylow3lem3  19425  lsmvalx  19435  txindislem  23021  xkoptsub  23042  fmfnfmlem3  23344  fmfnfmlem4  23345  ustuqtoplem  23628  ustuqtop0  23629  utopsnneiplem  23636  efabl  25943  efsubm  25944  addsunif  27353  perpln1  27715  perpln2  27716  isperp  27717  lmif  27790  islmib  27792  isgrpo  29502  grpoinvfval  29527  grpodivfval  29539  isvcOLD  29584  isnv  29617  abrexexd  31499  acunirnmpt  31642  acunirnmpt2  31643  acunirnmpt2f  31644  fnpreimac  31654  rnexd  31662  locfinreflem  32510  esumrnmpt2  32756  sxsigon  32880  omssubadd  32989  carsgclctunlem2  33008  pmeasadd  33014  sitgclg  33031  bnj1366  33530  ptrest  36150  elghomlem1OLD  36417  elghomlem2OLD  36418  isrngod  36430  iscringd  36530  imaexALTV  36864  xrnresex  36941  dfcnvrefrels2  37063  dfcnvrefrels3  37064  sticksstones3  40629  lmhmlnmsplit  41472  rclexi  42009  rtrclexlem  42010  trclubgNEW  42012  cnvrcl0  42019  dfrtrcl5  42023  relexpmulg  42104  relexp01min  42107  relexpxpmin  42111  unirnmap  43550  unirnmapsn  43556  ssmapsn  43558  fourierdlem70  44537  fourierdlem71  44538  fourierdlem80  44547  meadjiunlem  44826  omeiunle  44878  fexafv2ex  45572