Theorem rnex 7862

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, 7-Jul-2008.)

Hypothesis

Ref	Expression
dmex.1	⊢ 𝐴 ∈ V

Assertion

Ref	Expression
rnex	⊢ ran 𝐴 ∈ V

Proof of Theorem rnex

Step	Hyp	Ref	Expression
1		dmex.1	. 2 ⊢ 𝐴 ∈ V
2		rnexg 7854	. 2 ⊢ (𝐴 ∈ V → ran 𝐴 ∈ V)
3	1, 2	ax-mp 5	1 ⊢ ran 𝐴 ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3442  ran crn 5633

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379  ax-un 7690

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-cnv 5640  df-dm 5642  df-rn 5643

This theorem is referenced by:  elxp4  7874  elxp5  7875  ffoss  7900  fvclex  7913  wemoiso2  7928  2ndval  7946  fo2nd  7964  mapfoss  8801  ixpsnf1o  8888  bren  8905  mapen  9081  ssenen  9091  sucdom2  9139  fodomfib  9241  fodomfibOLD  9243  hartogslem1  9459  brwdom  9484  unxpwdom2  9505  noinfep  9581  r0weon  9934  fseqen  9949  acnlem  9970  infpwfien  9984  aceq3lem  10042  dfac4  10044  dfac5  10051  dfac2b  10053  dfac9  10059  dfac12lem2  10067  dfac12lem3  10068  infmap2  10139  cfflb  10181  infpssr  10230  fin23lem14  10255  fin23lem16  10257  fin23lem17  10260  fin23lem38  10271  fin23lem39  10272  axdc2lem  10370  axdc3lem2  10373  axcclem  10379  ttukeylem6  10436  wunex2  10661  wuncval2  10670  intgru  10737  wfgru  10739  qexALT  12889  seqexw  13952  shftfval  15005  vdwapval  16913  restfn  17356  prdsvallem  17386  prdsval  17387  wunfunc  17837  wunnat  17895  arwval  17979  catcfuccl  18054  catcxpccl  18142  yon11  18199  yon12  18200  yon2  18201  yonpropd  18203  oppcyon  18204  yonffth  18219  yoniso  18220  plusffval  18583  grpsubfval  18925  mulgfval  19011  sylow1lem2  19540  sylow2blem1  19561  sylow2blem2  19562  sylow3lem1  19568  sylow3lem6  19573  dmdprd  19941  dprdval  19946  staffval  20786  scaffval  20843  lpival  21291  ipffval  21615  cmpsub  23356  2ndcsep  23415  1stckgen  23510  kgencn2  23513  txcmplem1  23597  blbas  24386  met1stc  24477  psmetutop  24523  nmfval  24544  dchrptlem2  27244  dchrptlem3  27245  mulsproplem9  28132  ishpg  28843  edgval  29134  bafval  30692  vsfval  30721  foresf1o  32591  fnpreimac  32760  nsgmgc  33505  nsgqusf1o  33509  idlsrgtset  33601  locfinreflem  34018  cmpcref  34028  rspectopn  34045  ordtconnlem1  34102  qqhval  34150  sigapildsys  34340  dya2icoseg2  34456  dya2iocuni  34461  sxbrsigalem2  34464  sxbrsigalem5  34466  omssubadd  34478  mvtval  35716  mvrsval  35721  mstaval  35760  brrestrict  36165  relowlssretop  37618  exrecfnlem  37634  ctbssinf  37661  lindsdom  37865  indexdom  37985  heiborlem1  38062  isdrngo2  38209  isrngohom  38216  idlval  38264  isidl  38265  igenval  38312  lsatset  39366  dicval  41552  aks6d1c6isolem2  42545  prjcrvfval  42989  trclexi  43976  rtrclexi  43977  dfrtrcl5  43985  dfrcl2  44030  wfaxrep  45350  stoweidlem59  46417  fourierdlem71  46535  salgensscntex  46702  aacllem  50160