Theorem rnex 7886

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

Syntax hints:   ∈ wcel 2141  Vcvv 3453  ran crn 5644

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5243  ax-pr 5387  ax-un 7713

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-cnv 5651  df-dm 5653  df-rn 5654

This theorem is referenced by:  elxp4  7898  elxp5  7899  ffoss  7922  fvclex  7935  wemoiso2  7950  2ndval  7968  fo2nd  7986  mapfoss  8827  ixpsnf1o  8914  bren  8931  mapen  9107  ssenen  9117  sucdom2  9165  fodomfib  9267  fodomfibOLD  9268  hartogslem1  9484  brwdom  9509  unxpwdom2  9530  noinfep  9609  r0weon  9962  fseqen  9977  acnlem  9998  infpwfien  10012  aceq3lem  10070  dfac4  10072  dfac5  10079  dfac2b  10081  dfac9  10087  dfac12lem2  10095  dfac12lem3  10096  infmap2  10167  cfflb  10210  infpssr  10259  fin23lem14  10284  fin23lem16  10286  fin23lem17  10289  fin23lem38  10300  fin23lem39  10301  axdc2lem  10399  axdc3lem2  10402  axcclem  10408  ttukeylem6  10465  wunex2  10690  wuncval2  10699  intgru  10766  wfgru  10768  qexALT  12959  seqexw  14024  shftfval  15077  vdwapval  17000  restfn  17444  prdsvallem  17474  prdsval  17475  wunfunc  17925  wunnat  17983  arwval  18067  catcfuccl  18142  catcxpccl  18230  yon11  18287  yon12  18288  yon2  18289  yonpropd  18291  oppcyon  18292  yonffth  18307  yoniso  18308  plusffval  18671  grpsubfval  19016  mulgfval  19102  sylow1lem2  19630  sylow2blem1  19651  sylow2blem2  19652  sylow3lem1  19658  sylow3lem6  19663  dmdprd  20031  dprdval  20036  staffval  20878  scaffval  20935  lpival  21382  ipffval  21688  cmpsub  23448  2ndcsep  23507  1stckgen  23602  kgencn2  23605  txcmplem1  23689  blbas  24478  met1stc  24569  psmetutop  24615  nmfval  24636  dchrptlem2  27317  dchrptlem3  27318  mulsproplem9  28205  ishpg  28916  edgval  29207  bafval  30764  vsfval  30793  foresf1o  32663  fnpreimac  32833  nsgmgc  33559  nsgqusf1o  33563  idlsrgtset  33665  locfinreflem  34098  cmpcref  34108  rspectopn  34125  ordtconnlem1  34182  qqhval  34230  sigapildsys  34420  dya2icoseg2  34536  dya2iocuni  34541  sxbrsigalem2  34544  sxbrsigalem5  34546  omssubadd  34558  mvtval  35811  mvrsval  35816  mstaval  35855  brrestrict  36260  relowlssretop  37818  exrecfnlem  37834  ctbssinf  37861  lindsdom  38074  indexdom  38194  heiborlem1  38271  isdrngo2  38418  isrngohom  38425  idlval  38473  isidl  38474  igenval  38521  lsatset  39575  dicval  41761  aks6d1c6isolem2  42753  prjcrvfval  43174  trclexi  44157  rtrclexi  44158  dfrtrcl5  44166  dfrcl2  44211  wfaxrep  45531  stoweidlem59  46594  fourierdlem71  46712  salgensscntex  46879  aacllem  50383