Theorem rnex 7932

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 7924	. 2 ⊢ (𝐴 ∈ V → ran 𝐴 ∈ V)
3	1, 2	ax-mp 5	1 ⊢ ran 𝐴 ∈ V

Syntax hints:   ∈ wcel 2105  Vcvv 3477  ran crn 5689

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-cnv 5696  df-dm 5698  df-rn 5699

This theorem is referenced by:  elxp4  7944  elxp5  7945  ffoss  7968  fvclex  7981  wemoiso2  7997  2ndval  8015  fo2nd  8033  mapfoss  8890  ixpsnf1o  8976  bren  8993  sucdom2OLD  9120  mapen  9179  ssenen  9189  sucdom2  9240  fodomfib  9366  fodomfibOLD  9368  hartogslem1  9579  brwdom  9604  unxpwdom2  9625  noinfep  9697  r0weon  10049  fseqen  10064  acnlem  10085  infpwfien  10099  aceq3lem  10157  dfac4  10159  dfac5  10166  dfac2b  10168  dfac9  10174  dfac12lem2  10182  dfac12lem3  10183  infmap2  10254  cfflb  10296  infpssr  10345  fin23lem14  10370  fin23lem16  10372  fin23lem17  10375  fin23lem38  10386  fin23lem39  10387  axdc2lem  10485  axdc3lem2  10488  axcclem  10494  ttukeylem6  10551  wunex2  10775  wuncval2  10784  intgru  10851  wfgru  10853  qexALT  13003  seqexw  14054  shftfval  15105  vdwapval  17006  restfn  17470  prdsvallem  17500  prdsval  17501  wunfunc  17951  wunfuncOLD  17952  wunnat  18010  wunnatOLD  18011  arwval  18096  catcfuccl  18172  catcfucclOLD  18173  catcxpccl  18262  catcxpcclOLD  18263  yon11  18320  yon12  18321  yon2  18322  yonpropd  18324  oppcyon  18325  yonffth  18340  yoniso  18341  plusffval  18671  grpsubfval  19013  mulgfval  19099  sylow1lem2  19631  sylow2blem1  19652  sylow2blem2  19653  sylow3lem1  19659  sylow3lem6  19664  dmdprd  20032  dprdval  20037  staffval  20858  scaffval  20894  lpival  21351  ipffval  21683  cmpsub  23423  2ndcsep  23482  1stckgen  23577  kgencn2  23580  txcmplem1  23664  blbas  24455  met1stc  24549  psmetutop  24595  nmfval  24616  dchrptlem2  27323  dchrptlem3  27324  mulsproplem9  28164  ishpg  28781  edgval  29080  bafval  30632  vsfval  30661  foresf1o  32531  fnpreimac  32687  nsgmgc  33419  nsgqusf1o  33423  idlsrgtset  33515  locfinreflem  33800  cmpcref  33810  rspectopn  33827  ordtconnlem1  33884  qqhval  33934  sigapildsys  34142  dya2icoseg2  34259  dya2iocuni  34264  sxbrsigalem2  34267  sxbrsigalem5  34269  omssubadd  34281  mvtval  35484  mvrsval  35489  mstaval  35528  brrestrict  35930  relowlssretop  37345  exrecfnlem  37361  ctbssinf  37388  lindsdom  37600  indexdom  37720  heiborlem1  37797  isdrngo2  37944  isrngohom  37951  idlval  37999  isidl  38000  igenval  38047  lsatset  38971  dicval  41158  aks6d1c6isolem2  42156  prjcrvfval  42617  trclexi  43609  rtrclexi  43610  dfrtrcl5  43618  dfrcl2  43663  wfaxrep  44949  stoweidlem59  46014  fourierdlem71  46132  salgensscntex  46299  aacllem  49031