Theorem rnex 7759

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

Syntax hints:   ∈ wcel 2106  Vcvv 3432  ran crn 5590

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-cnv 5597  df-dm 5599  df-rn 5600

This theorem is referenced by:  elxp4  7769  elxp5  7770  ffoss  7788  fvclex  7801  wemoiso2  7817  2ndval  7834  fo2nd  7852  mapfoss  8640  ixpsnf1o  8726  bren  8743  brenOLD  8744  sucdom2OLD  8869  mapen  8928  ssenen  8938  sucdom2  8989  fodomfib  9093  hartogslem1  9301  brwdom  9326  unxpwdom2  9347  noinfep  9418  r0weon  9768  fseqen  9783  acnlem  9804  infpwfien  9818  aceq3lem  9876  dfac4  9878  dfac5  9884  dfac2b  9886  dfac9  9892  dfac12lem2  9900  dfac12lem3  9901  infmap2  9974  cfflb  10015  infpssr  10064  fin23lem14  10089  fin23lem16  10091  fin23lem17  10094  fin23lem38  10105  fin23lem39  10106  axdc2lem  10204  axdc3lem2  10207  axcclem  10213  ttukeylem6  10270  wunex2  10494  wuncval2  10503  intgru  10570  wfgru  10572  qexALT  12704  seqexw  13737  hashfacenOLD  14167  shftfval  14781  vdwapval  16674  restfn  17135  prdsvallem  17165  prdsval  17166  wunfunc  17614  wunfuncOLD  17615  wunnat  17672  wunnatOLD  17673  arwval  17758  catcfuccl  17834  catcfucclOLD  17835  catcxpccl  17924  catcxpcclOLD  17925  yon11  17982  yon12  17983  yon2  17984  yonpropd  17986  oppcyon  17987  yonffth  18002  yoniso  18003  plusffval  18332  grpsubfval  18623  mulgfval  18702  sylow1lem2  19204  sylow2blem1  19225  sylow2blem2  19226  sylow3lem1  19232  sylow3lem6  19237  dmdprd  19601  dprdval  19606  staffval  20107  scaffval  20141  lpival  20516  ipffval  20853  cmpsub  22551  2ndcsep  22610  1stckgen  22705  kgencn2  22708  txcmplem1  22792  blbas  23583  met1stc  23677  psmetutop  23723  nmfval  23744  dchrptlem2  26413  dchrptlem3  26414  ishpg  27120  edgval  27419  bafval  28966  vsfval  28995  foresf1o  30850  fnpreimac  31008  nsgmgc  31597  nsgqusf1o  31601  idlsrgtset  31653  locfinreflem  31790  cmpcref  31800  rspectopn  31817  ordtconnlem1  31874  qqhval  31924  sigapildsys  32130  dya2icoseg2  32245  dya2iocuni  32250  sxbrsigalem2  32253  sxbrsigalem5  32255  omssubadd  32267  mvtval  33462  mvrsval  33467  mstaval  33506  brrestrict  34251  relowlssretop  35534  exrecfnlem  35550  ctbssinf  35577  lindsdom  35771  indexdom  35892  heiborlem1  35969  isdrngo2  36116  isrngohom  36123  idlval  36171  isidl  36172  igenval  36219  lsatset  37004  dicval  39190  prjcrvfval  40468  trclexi  41228  rtrclexi  41229  dfrtrcl5  41237  dfrcl2  41282  stoweidlem59  43600  fourierdlem71  43718  salgensscntex  43883  aacllem  46505