Theorem rnex 7733

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

Syntax hints:   ∈ wcel 2108  Vcvv 3422  ran crn 5581

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347  ax-un 7566

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-cnv 5588  df-dm 5590  df-rn 5591

This theorem is referenced by:  elxp4  7743  elxp5  7744  ffoss  7762  fvclex  7775  wemoiso2  7790  2ndval  7807  fo2nd  7825  mapfoss  8598  ixpsnf1o  8684  bren  8701  brenOLD  8702  sucdom2  8822  mapen  8877  ssenen  8887  fodomfib  9023  hartogslem1  9231  brwdom  9256  unxpwdom2  9277  noinfep  9348  trpredex  9416  r0weon  9699  fseqen  9714  acnlem  9735  infpwfien  9749  aceq3lem  9807  dfac4  9809  dfac5  9815  dfac2b  9817  dfac9  9823  dfac12lem2  9831  dfac12lem3  9832  infmap2  9905  cfflb  9946  infpssr  9995  fin23lem14  10020  fin23lem16  10022  fin23lem17  10025  fin23lem38  10036  fin23lem39  10037  axdc2lem  10135  axdc3lem2  10138  axcclem  10144  ttukeylem6  10201  wunex2  10425  wuncval2  10434  intgru  10501  wfgru  10503  qexALT  12633  seqexw  13665  hashfacenOLD  14095  shftfval  14709  vdwapval  16602  restfn  17052  prdsvallem  17082  prdsval  17083  wunfunc  17530  wunfuncOLD  17531  wunnat  17588  wunnatOLD  17589  arwval  17674  catcfuccl  17750  catcfucclOLD  17751  catcxpccl  17840  catcxpcclOLD  17841  yon11  17898  yon12  17899  yon2  17900  yonpropd  17902  oppcyon  17903  yonffth  17918  yoniso  17919  plusffval  18247  grpsubfval  18538  mulgfval  18617  sylow1lem2  19119  sylow2blem1  19140  sylow2blem2  19141  sylow3lem1  19147  sylow3lem6  19152  dmdprd  19516  dprdval  19521  staffval  20022  scaffval  20056  lpival  20429  ipffval  20765  cmpsub  22459  2ndcsep  22518  1stckgen  22613  kgencn2  22616  txcmplem1  22700  blbas  23491  met1stc  23583  psmetutop  23629  nmfval  23650  dchrptlem2  26318  dchrptlem3  26319  ishpg  27024  edgval  27322  bafval  28867  vsfval  28896  foresf1o  30751  fnpreimac  30910  nsgmgc  31499  nsgqusf1o  31503  idlsrgtset  31555  locfinreflem  31692  cmpcref  31702  rspectopn  31719  ordtconnlem1  31776  qqhval  31824  sigapildsys  32030  dya2icoseg2  32145  dya2iocuni  32150  sxbrsigalem2  32153  sxbrsigalem5  32155  omssubadd  32167  mvtval  33362  mvrsval  33367  mstaval  33406  brrestrict  34178  relowlssretop  35461  exrecfnlem  35477  ctbssinf  35504  lindsdom  35698  indexdom  35819  heiborlem1  35896  isdrngo2  36043  isrngohom  36050  idlval  36098  isidl  36099  igenval  36146  lsatset  36931  dicval  39117  trclexi  41117  rtrclexi  41118  dfrtrcl5  41126  dfrcl2  41171  stoweidlem59  43490  fourierdlem71  43608  salgensscntex  43773  aacllem  46391