Theorem rnex 7849

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

Syntax hints:   ∈ wcel 2113  Vcvv 3437  ran crn 5622

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 2115  ax-9 2123  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7677

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 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-cnv 5629  df-dm 5631  df-rn 5632

This theorem is referenced by:  elxp4  7861  elxp5  7862  ffoss  7887  fvclex  7900  wemoiso2  7915  2ndval  7933  fo2nd  7951  mapfoss  8785  ixpsnf1o  8872  bren  8889  mapen  9065  ssenen  9075  sucdom2  9123  fodomfib  9224  fodomfibOLD  9226  hartogslem1  9439  brwdom  9464  unxpwdom2  9485  noinfep  9561  r0weon  9914  fseqen  9929  acnlem  9950  infpwfien  9964  aceq3lem  10022  dfac4  10024  dfac5  10031  dfac2b  10033  dfac9  10039  dfac12lem2  10047  dfac12lem3  10048  infmap2  10119  cfflb  10161  infpssr  10210  fin23lem14  10235  fin23lem16  10237  fin23lem17  10240  fin23lem38  10251  fin23lem39  10252  axdc2lem  10350  axdc3lem2  10353  axcclem  10359  ttukeylem6  10416  wunex2  10640  wuncval2  10649  intgru  10716  wfgru  10718  qexALT  12868  seqexw  13931  shftfval  14984  vdwapval  16892  restfn  17335  prdsvallem  17365  prdsval  17366  wunfunc  17816  wunnat  17874  arwval  17958  catcfuccl  18033  catcxpccl  18121  yon11  18178  yon12  18179  yon2  18180  yonpropd  18182  oppcyon  18183  yonffth  18198  yoniso  18199  plusffval  18562  grpsubfval  18904  mulgfval  18990  sylow1lem2  19519  sylow2blem1  19540  sylow2blem2  19541  sylow3lem1  19547  sylow3lem6  19552  dmdprd  19920  dprdval  19925  staffval  20765  scaffval  20822  lpival  21270  ipffval  21594  cmpsub  23335  2ndcsep  23394  1stckgen  23489  kgencn2  23492  txcmplem1  23576  blbas  24365  met1stc  24456  psmetutop  24502  nmfval  24523  dchrptlem2  27223  dchrptlem3  27224  mulsproplem9  28083  ishpg  28757  edgval  29048  bafval  30605  vsfval  30634  foresf1o  32505  fnpreimac  32675  nsgmgc  33421  nsgqusf1o  33425  idlsrgtset  33517  locfinreflem  33925  cmpcref  33935  rspectopn  33952  ordtconnlem1  34009  qqhval  34057  sigapildsys  34247  dya2icoseg2  34363  dya2iocuni  34368  sxbrsigalem2  34371  sxbrsigalem5  34373  omssubadd  34385  mvtval  35616  mvrsval  35621  mstaval  35660  brrestrict  36065  relowlssretop  37480  exrecfnlem  37496  ctbssinf  37523  lindsdom  37727  indexdom  37847  heiborlem1  37924  isdrngo2  38071  isrngohom  38078  idlval  38126  isidl  38127  igenval  38174  lsatset  39162  dicval  41348  aks6d1c6isolem2  42341  prjcrvfval  42789  trclexi  43777  rtrclexi  43778  dfrtrcl5  43786  dfrcl2  43831  wfaxrep  45151  stoweidlem59  46219  fourierdlem71  46337  salgensscntex  46504  aacllem  49962