Theorem rnex 7843

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

Syntax hints:   ∈ wcel 2109  Vcvv 3436  ran crn 5620

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371  ax-un 7671

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3395  df-v 3438  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-cnv 5627  df-dm 5629  df-rn 5630

This theorem is referenced by:  elxp4  7855  elxp5  7856  ffoss  7881  fvclex  7894  wemoiso2  7909  2ndval  7927  fo2nd  7945  mapfoss  8779  ixpsnf1o  8865  bren  8882  mapen  9058  ssenen  9068  sucdom2  9117  fodomfib  9219  fodomfibOLD  9221  hartogslem1  9434  brwdom  9459  unxpwdom2  9480  noinfep  9556  r0weon  9906  fseqen  9921  acnlem  9942  infpwfien  9956  aceq3lem  10014  dfac4  10016  dfac5  10023  dfac2b  10025  dfac9  10031  dfac12lem2  10039  dfac12lem3  10040  infmap2  10111  cfflb  10153  infpssr  10202  fin23lem14  10227  fin23lem16  10229  fin23lem17  10232  fin23lem38  10243  fin23lem39  10244  axdc2lem  10342  axdc3lem2  10345  axcclem  10351  ttukeylem6  10408  wunex2  10632  wuncval2  10641  intgru  10708  wfgru  10710  qexALT  12865  seqexw  13924  shftfval  14977  vdwapval  16885  restfn  17328  prdsvallem  17358  prdsval  17359  wunfunc  17808  wunnat  17866  arwval  17950  catcfuccl  18025  catcxpccl  18113  yon11  18170  yon12  18171  yon2  18172  yonpropd  18174  oppcyon  18175  yonffth  18190  yoniso  18191  plusffval  18520  grpsubfval  18862  mulgfval  18948  sylow1lem2  19478  sylow2blem1  19499  sylow2blem2  19500  sylow3lem1  19506  sylow3lem6  19511  dmdprd  19879  dprdval  19884  staffval  20726  scaffval  20783  lpival  21231  ipffval  21555  cmpsub  23285  2ndcsep  23344  1stckgen  23439  kgencn2  23442  txcmplem1  23526  blbas  24316  met1stc  24407  psmetutop  24453  nmfval  24474  dchrptlem2  27174  dchrptlem3  27175  mulsproplem9  28032  ishpg  28704  edgval  28994  bafval  30548  vsfval  30577  foresf1o  32448  fnpreimac  32614  nsgmgc  33349  nsgqusf1o  33353  idlsrgtset  33445  locfinreflem  33807  cmpcref  33817  rspectopn  33834  ordtconnlem1  33891  qqhval  33939  sigapildsys  34129  dya2icoseg2  34246  dya2iocuni  34251  sxbrsigalem2  34254  sxbrsigalem5  34256  omssubadd  34268  mvtval  35473  mvrsval  35478  mstaval  35517  brrestrict  35923  relowlssretop  37337  exrecfnlem  37353  ctbssinf  37380  lindsdom  37594  indexdom  37714  heiborlem1  37791  isdrngo2  37938  isrngohom  37945  idlval  37993  isidl  37994  igenval  38041  lsatset  38969  dicval  41155  aks6d1c6isolem2  42148  prjcrvfval  42604  trclexi  43593  rtrclexi  43594  dfrtrcl5  43602  dfrcl2  43647  wfaxrep  44968  stoweidlem59  46040  fourierdlem71  46158  salgensscntex  46325  aacllem  49786