Theorem rnex 7835

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

Syntax hints:   ∈ wcel 2111  Vcvv 3436  ran crn 5612

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365  ax-un 7663

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-opab 5149  df-cnv 5619  df-dm 5621  df-rn 5622

This theorem is referenced by:  elxp4  7847  elxp5  7848  ffoss  7873  fvclex  7886  wemoiso2  7901  2ndval  7919  fo2nd  7937  mapfoss  8771  ixpsnf1o  8857  bren  8874  mapen  9049  ssenen  9059  sucdom2  9107  fodomfib  9208  fodomfibOLD  9210  hartogslem1  9423  brwdom  9448  unxpwdom2  9469  noinfep  9545  r0weon  9898  fseqen  9913  acnlem  9934  infpwfien  9948  aceq3lem  10006  dfac4  10008  dfac5  10015  dfac2b  10017  dfac9  10023  dfac12lem2  10031  dfac12lem3  10032  infmap2  10103  cfflb  10145  infpssr  10194  fin23lem14  10219  fin23lem16  10221  fin23lem17  10224  fin23lem38  10235  fin23lem39  10236  axdc2lem  10334  axdc3lem2  10337  axcclem  10343  ttukeylem6  10400  wunex2  10624  wuncval2  10633  intgru  10700  wfgru  10702  qexALT  12857  seqexw  13919  shftfval  14972  vdwapval  16880  restfn  17323  prdsvallem  17353  prdsval  17354  wunfunc  17803  wunnat  17861  arwval  17945  catcfuccl  18020  catcxpccl  18108  yon11  18165  yon12  18166  yon2  18167  yonpropd  18169  oppcyon  18170  yonffth  18185  yoniso  18186  plusffval  18549  grpsubfval  18891  mulgfval  18977  sylow1lem2  19506  sylow2blem1  19527  sylow2blem2  19528  sylow3lem1  19534  sylow3lem6  19539  dmdprd  19907  dprdval  19912  staffval  20751  scaffval  20808  lpival  21256  ipffval  21580  cmpsub  23310  2ndcsep  23369  1stckgen  23464  kgencn2  23467  txcmplem1  23551  blbas  24340  met1stc  24431  psmetutop  24477  nmfval  24498  dchrptlem2  27198  dchrptlem3  27199  mulsproplem9  28058  ishpg  28732  edgval  29022  bafval  30576  vsfval  30605  foresf1o  32476  fnpreimac  32645  nsgmgc  33369  nsgqusf1o  33373  idlsrgtset  33465  locfinreflem  33845  cmpcref  33855  rspectopn  33872  ordtconnlem1  33929  qqhval  33977  sigapildsys  34167  dya2icoseg2  34283  dya2iocuni  34288  sxbrsigalem2  34291  sxbrsigalem5  34293  omssubadd  34305  mvtval  35536  mvrsval  35541  mstaval  35580  brrestrict  35983  relowlssretop  37397  exrecfnlem  37413  ctbssinf  37440  lindsdom  37654  indexdom  37774  heiborlem1  37851  isdrngo2  37998  isrngohom  38005  idlval  38053  isidl  38054  igenval  38101  lsatset  39029  dicval  41215  aks6d1c6isolem2  42208  prjcrvfval  42664  trclexi  43653  rtrclexi  43654  dfrtrcl5  43662  dfrcl2  43707  wfaxrep  45027  stoweidlem59  46097  fourierdlem71  46215  salgensscntex  46382  aacllem  49833