Theorem rnex 7903

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

Syntax hints:   ∈ wcel 2149  Vcvv 3463  ran crn 5660

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5258  ax-pr 5402  ax-un 7730

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-cnv 5667  df-dm 5669  df-rn 5670

This theorem is referenced by:  elxp4  7915  elxp5  7916  ffoss  7939  fvclex  7952  wemoiso2  7967  2ndval  7985  fo2nd  8003  mapfoss  8845  ixpsnf1o  8932  bren  8949  mapen  9125  ssenen  9135  sucdom2  9183  fodomfib  9284  hartogslem1  9500  brwdom  9525  unxpwdom2  9546  noinfep  9625  r0weon  9992  fseqen  10007  acnlem  10028  infpwfien  10042  aceq3lem  10100  dfac4  10102  dfac5  10108  dfac2b  10110  dfac9  10116  dfac12lem2  10124  dfac12lem3  10125  infmap2  10196  cfflb  10239  infpssr  10288  fin23lem14  10313  fin23lem16  10315  fin23lem17  10318  fin23lem38  10329  fin23lem39  10330  axdc2lem  10428  axdc3lem2  10431  axcclem  10437  ttukeylem6  10494  wunex2  10719  wuncval2  10728  intgru  10795  wfgru  10797  qexALT  12984  seqexw  14049  shftfval  15103  vdwapval  17029  restfn  17473  prdsvallem  17503  prdsval  17504  wunfunc  17954  wunnat  18012  arwval  18096  catcfuccl  18171  catcxpccl  18259  yon11  18316  yon12  18317  yon2  18318  yonpropd  18320  oppcyon  18321  yonffth  18336  yoniso  18337  plusffval  18700  grpsubfval  19046  mulgfval  19131  sylow1lem2  19665  sylow2blem1  19686  sylow2blem2  19687  sylow3lem1  19693  sylow3lem6  19698  dmdprd  20066  dprdval  20071  staffval  20918  scaffval  20975  lpival  21457  ipffval  21763  cmpsub  23522  2ndcsep  23581  1stckgen  23676  kgencn2  23679  txcmplem1  23763  blbas  24552  met1stc  24643  psmetutop  24689  nmfval  24710  dchrptlem2  27391  dchrptlem3  27392  mulsproplem9  28279  ishpg  28996  tgplnfn  29011  plngval  29013  isplng  29014  brprlng  29139  edgval  29336  bafval  30893  vsfval  30922  foresf1o  32787  fnpreimac  32952  nsgmgc  33661  nsgqusf1o  33665  idlsrgtset  33739  locfinreflem  34171  cmpcref  34181  rspectopn  34198  ordtconnlem1  34255  qqhval  34303  sigapildsys  34493  dya2icoseg2  34609  dya2iocuni  34614  sxbrsigalem2  34617  sxbrsigalem5  34619  omssubadd  34631  mvtval  35887  mvrsval  35892  mstaval  35931  brrestrict  36336  relowlssretop  37892  exrecfnlem  37908  ctbssinf  37935  lindsdom  38148  indexdom  38268  heiborlem1  38345  isdrngo2  38492  isrngohom  38499  idlval  38547  isidl  38548  igenval  38595  lsatset  39649  dicval  41835  aks6d1c6isolem2  42827  prjcrvfval  43250  trclexi  44233  rtrclexi  44234  dfrtrcl5  44242  dfrcl2  44287  wfaxrep  45590  stoweidlem59  46660  fourierdlem71  46778  salgensscntex  46945  aacllem  50470