Theorem rnex 7905

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 7897	. 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 7727

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  7915  elxp5  7916  ffoss  7934  fvclex  7947  wemoiso2  7963  2ndval  7980  fo2nd  7998  mapfoss  8848  ixpsnf1o  8934  bren  8951  brenOLD  8952  sucdom2OLD  9084  mapen  9143  ssenen  9153  sucdom2  9208  fodomfib  9328  hartogslem1  9539  brwdom  9564  unxpwdom2  9585  noinfep  9657  r0weon  10009  fseqen  10024  acnlem  10045  infpwfien  10059  aceq3lem  10117  dfac4  10119  dfac5  10125  dfac2b  10127  dfac9  10133  dfac12lem2  10141  dfac12lem3  10142  infmap2  10215  cfflb  10256  infpssr  10305  fin23lem14  10330  fin23lem16  10332  fin23lem17  10335  fin23lem38  10346  fin23lem39  10347  axdc2lem  10445  axdc3lem2  10448  axcclem  10454  ttukeylem6  10511  wunex2  10735  wuncval2  10744  intgru  10811  wfgru  10813  qexALT  12950  seqexw  13984  hashfacenOLD  14416  shftfval  15019  vdwapval  16908  restfn  17372  prdsvallem  17402  prdsval  17403  wunfunc  17851  wunfuncOLD  17852  wunnat  17909  wunnatOLD  17910  arwval  17995  catcfuccl  18071  catcfucclOLD  18072  catcxpccl  18161  catcxpcclOLD  18162  yon11  18219  yon12  18220  yon2  18221  yonpropd  18223  oppcyon  18224  yonffth  18239  yoniso  18240  plusffval  18569  grpsubfval  18870  mulgfval  18954  sylow1lem2  19469  sylow2blem1  19490  sylow2blem2  19491  sylow3lem1  19497  sylow3lem6  19502  dmdprd  19870  dprdval  19875  staffval  20459  scaffval  20495  lpival  20889  ipffval  21207  cmpsub  22911  2ndcsep  22970  1stckgen  23065  kgencn2  23068  txcmplem1  23152  blbas  23943  met1stc  24037  psmetutop  24083  nmfval  24104  dchrptlem2  26775  dchrptlem3  26776  mulsproplem9  27590  ishpg  28048  edgval  28347  bafval  29895  vsfval  29924  foresf1o  31780  fnpreimac  31934  nsgmgc  32568  nsgqusf1o  32572  idlsrgtset  32667  locfinreflem  32889  cmpcref  32899  rspectopn  32916  ordtconnlem1  32973  qqhval  33023  sigapildsys  33229  dya2icoseg2  33346  dya2iocuni  33351  sxbrsigalem2  33354  sxbrsigalem5  33356  omssubadd  33368  mvtval  34560  mvrsval  34565  mstaval  34604  brrestrict  34996  relowlssretop  36336  exrecfnlem  36352  ctbssinf  36379  lindsdom  36574  indexdom  36694  heiborlem1  36771  isdrngo2  36918  isrngohom  36925  idlval  36973  isidl  36974  igenval  37021  lsatset  37952  dicval  40139  prjcrvfval  41461  trclexi  42459  rtrclexi  42460  dfrtrcl5  42468  dfrcl2  42513  stoweidlem59  44860  fourierdlem71  44978  salgensscntex  45145  aacllem  47932