Theorem rnex 7902

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

Syntax hints:   ∈ wcel 2106  Vcvv 3474  ran crn 5677

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 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7724

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 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-cnv 5684  df-dm 5686  df-rn 5687

This theorem is referenced by:  elxp4  7912  elxp5  7913  ffoss  7931  fvclex  7944  wemoiso2  7960  2ndval  7977  fo2nd  7995  mapfoss  8845  ixpsnf1o  8931  bren  8948  brenOLD  8949  sucdom2OLD  9081  mapen  9140  ssenen  9150  sucdom2  9205  fodomfib  9325  hartogslem1  9536  brwdom  9561  unxpwdom2  9582  noinfep  9654  r0weon  10006  fseqen  10021  acnlem  10042  infpwfien  10056  aceq3lem  10114  dfac4  10116  dfac5  10122  dfac2b  10124  dfac9  10130  dfac12lem2  10138  dfac12lem3  10139  infmap2  10212  cfflb  10253  infpssr  10302  fin23lem14  10327  fin23lem16  10329  fin23lem17  10332  fin23lem38  10343  fin23lem39  10344  axdc2lem  10442  axdc3lem2  10445  axcclem  10451  ttukeylem6  10508  wunex2  10732  wuncval2  10741  intgru  10808  wfgru  10810  qexALT  12947  seqexw  13981  hashfacenOLD  14413  shftfval  15016  vdwapval  16905  restfn  17369  prdsvallem  17399  prdsval  17400  wunfunc  17848  wunfuncOLD  17849  wunnat  17906  wunnatOLD  17907  arwval  17992  catcfuccl  18068  catcfucclOLD  18069  catcxpccl  18158  catcxpcclOLD  18159  yon11  18216  yon12  18217  yon2  18218  yonpropd  18220  oppcyon  18221  yonffth  18236  yoniso  18237  plusffval  18566  grpsubfval  18867  mulgfval  18951  sylow1lem2  19466  sylow2blem1  19487  sylow2blem2  19488  sylow3lem1  19494  sylow3lem6  19499  dmdprd  19867  dprdval  19872  staffval  20454  scaffval  20489  lpival  20882  ipffval  21200  cmpsub  22903  2ndcsep  22962  1stckgen  23057  kgencn2  23060  txcmplem1  23144  blbas  23935  met1stc  24029  psmetutop  24075  nmfval  24096  dchrptlem2  26765  dchrptlem3  26766  mulsproplem9  27577  ishpg  28007  edgval  28306  bafval  29852  vsfval  29881  foresf1o  31737  fnpreimac  31891  nsgmgc  32518  nsgqusf1o  32522  idlsrgtset  32617  locfinreflem  32815  cmpcref  32825  rspectopn  32842  ordtconnlem1  32899  qqhval  32949  sigapildsys  33155  dya2icoseg2  33272  dya2iocuni  33277  sxbrsigalem2  33280  sxbrsigalem5  33282  omssubadd  33294  mvtval  34486  mvrsval  34491  mstaval  34530  brrestrict  34916  relowlssretop  36239  exrecfnlem  36255  ctbssinf  36282  lindsdom  36477  indexdom  36597  heiborlem1  36674  isdrngo2  36821  isrngohom  36828  idlval  36876  isidl  36877  igenval  36924  lsatset  37855  dicval  40042  prjcrvfval  41374  trclexi  42361  rtrclexi  42362  dfrtrcl5  42370  dfrcl2  42415  stoweidlem59  44765  fourierdlem71  44883  salgensscntex  45050  aacllem  47838