Theorem rnex 7933

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

Syntax hints:   ∈ wcel 2107  Vcvv 3479  ran crn 5685

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707  ax-sep 5295  ax-nul 5305  ax-pr 5431  ax-un 7756

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4907  df-br 5143  df-opab 5205  df-cnv 5692  df-dm 5694  df-rn 5695

This theorem is referenced by:  elxp4  7945  elxp5  7946  ffoss  7971  fvclex  7984  wemoiso2  8000  2ndval  8018  fo2nd  8036  mapfoss  8893  ixpsnf1o  8979  bren  8996  sucdom2OLD  9123  mapen  9182  ssenen  9192  sucdom2  9244  fodomfib  9370  fodomfibOLD  9372  hartogslem1  9583  brwdom  9608  unxpwdom2  9629  noinfep  9701  r0weon  10053  fseqen  10068  acnlem  10089  infpwfien  10103  aceq3lem  10161  dfac4  10163  dfac5  10170  dfac2b  10172  dfac9  10178  dfac12lem2  10186  dfac12lem3  10187  infmap2  10258  cfflb  10300  infpssr  10349  fin23lem14  10374  fin23lem16  10376  fin23lem17  10379  fin23lem38  10390  fin23lem39  10391  axdc2lem  10489  axdc3lem2  10492  axcclem  10498  ttukeylem6  10555  wunex2  10779  wuncval2  10788  intgru  10855  wfgru  10857  qexALT  13007  seqexw  14059  shftfval  15110  vdwapval  17012  restfn  17470  prdsvallem  17500  prdsval  17501  wunfunc  17947  wunnat  18005  arwval  18089  catcfuccl  18164  catcxpccl  18253  yon11  18310  yon12  18311  yon2  18312  yonpropd  18314  oppcyon  18315  yonffth  18330  yoniso  18331  plusffval  18660  grpsubfval  19002  mulgfval  19088  sylow1lem2  19618  sylow2blem1  19639  sylow2blem2  19640  sylow3lem1  19646  sylow3lem6  19651  dmdprd  20019  dprdval  20024  staffval  20843  scaffval  20879  lpival  21335  ipffval  21667  cmpsub  23409  2ndcsep  23468  1stckgen  23563  kgencn2  23566  txcmplem1  23650  blbas  24441  met1stc  24535  psmetutop  24581  nmfval  24602  dchrptlem2  27310  dchrptlem3  27311  mulsproplem9  28151  ishpg  28768  edgval  29067  bafval  30624  vsfval  30653  foresf1o  32524  fnpreimac  32682  nsgmgc  33441  nsgqusf1o  33445  idlsrgtset  33537  locfinreflem  33840  cmpcref  33850  rspectopn  33867  ordtconnlem1  33924  qqhval  33974  sigapildsys  34164  dya2icoseg2  34281  dya2iocuni  34286  sxbrsigalem2  34289  sxbrsigalem5  34291  omssubadd  34303  mvtval  35506  mvrsval  35511  mstaval  35550  brrestrict  35951  relowlssretop  37365  exrecfnlem  37381  ctbssinf  37408  lindsdom  37622  indexdom  37742  heiborlem1  37819  isdrngo2  37966  isrngohom  37973  idlval  38021  isidl  38022  igenval  38069  lsatset  38992  dicval  41179  aks6d1c6isolem2  42177  prjcrvfval  42646  trclexi  43638  rtrclexi  43639  dfrtrcl5  43647  dfrcl2  43692  wfaxrep  45016  stoweidlem59  46079  fourierdlem71  46197  salgensscntex  46364  aacllem  49375