Theorem rnex 7903

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

Syntax hints:   ∈ wcel 2143  Vcvv 3455  ran crn 5662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404  ax-un 7732

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-cnv 5669  df-dm 5671  df-rn 5672

This theorem is referenced by:  elxp4  7915  elxp5  7916  ffoss  7939  fvclex  7952  wemoiso2  7967  2ndval  7985  fo2nd  8003  mapfoss  8845  ixpsnf1o  8932  bren  8949  mapen  9125  ssenen  9135  sucdom2  9183  fodomfib  9284  hartogslem1  9500  brwdom  9525  unxpwdom2  9546  noinfep  9625  r0weon  9992  fseqen  10007  acnlem  10028  infpwfien  10042  aceq3lem  10100  dfac4  10102  dfac5  10108  dfac2b  10110  dfac9  10116  dfac12lem2  10124  dfac12lem3  10125  infmap2  10196  cfflb  10238  infpssr  10287  fin23lem14  10312  fin23lem16  10314  fin23lem17  10317  fin23lem38  10328  fin23lem39  10329  axdc2lem  10427  axdc3lem2  10430  axcclem  10436  ttukeylem6  10493  wunex2  10718  wuncval2  10727  intgru  10794  wfgru  10796  qexALT  12983  seqexw  14049  shftfval  15103  vdwapval  17028  restfn  17472  prdsvallem  17502  prdsval  17503  wunfunc  17953  wunnat  18011  arwval  18095  catcfuccl  18170  catcxpccl  18258  yon11  18315  yon12  18316  yon2  18317  yonpropd  18319  oppcyon  18320  yonffth  18335  yoniso  18336  plusffval  18699  grpsubfval  19045  mulgfval  19130  sylow1lem2  19664  sylow2blem1  19685  sylow2blem2  19686  sylow3lem1  19692  sylow3lem6  19697  dmdprd  20065  dprdval  20070  staffval  20944  scaffval  21001  lpival  21492  ipffval  21798  cmpsub  23557  2ndcsep  23616  1stckgen  23711  kgencn2  23714  txcmplem1  23798  blbas  24587  met1stc  24678  psmetutop  24724  nmfval  24745  dchrptlem2  27429  dchrptlem3  27430  mulsproplem9  28317  ishpg  29041  tgplnfn  29057  plngval  29059  isplng  29060  brprlng  29188  edgval  29399  bafval  30956  vsfval  30985  foresf1o  32850  fnpreimac  33015  nsgmgc  33721  nsgqusf1o  33725  idlsrgtset  33798  locfinreflem  34230  cmpcref  34240  rspectopn  34257  ordtconnlem1  34314  qqhval  34362  sigapildsys  34552  dya2icoseg2  34668  dya2iocuni  34673  sxbrsigalem2  34676  sxbrsigalem5  34678  omssubadd  34690  mvtval  35992  mvrsval  35997  mstaval  36036  brrestrict  36441  relowlssretop  38009  exrecfnlem  38025  ctbssinf  38052  lindsdom  38265  indexdom  38385  heiborlem1  38462  isdrngo2  38609  isrngohom  38616  idlval  38664  isidl  38665  igenval  38712  lsatset  39764  dicval  41950  aks6d1c6isolem2  42942  prjcrvfval  43363  trclexi  44346  rtrclexi  44347  dfrtrcl5  44355  dfrcl2  44400  wfaxrep  45703  stoweidlem59  46773  fourierdlem71  46891  salgensscntex  47058  aacllem  50621