Theorem rnex 7907

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3450  ran crn 5656

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pr 5398  ax-un 7736

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-cnv 5663  df-dm 5665  df-rn 5666

This theorem is used by:  elxp4  7919  elxp5  7920  ffoss  7943  fvclex  7956  wemoiso2  7971  2ndval  7989  fo2nd  8007  mapfoss  8853  ixpsnf1o  8945  bren  8962  mapen  9139  ssenen  9149  sucdom2  9197  fodomfib  9298  hartogslem1  9514  brwdom  9539  unxpwdom2  9560  noinfep  9639  r0weon  10015  fseqen  10030  acnlem  10051  infpwfien  10065  aceq3lem  10123  dfac4  10125  dfac5  10131  dfac2b  10133  dfac9  10139  dfac12lem2  10147  dfac12lem3  10148  infmap2  10219  cfflb  10261  infpssr  10310  fin23lem14  10335  fin23lem16  10337  fin23lem17  10340  fin23lem38  10351  fin23lem39  10352  axdc2lem  10450  axdc3lem2  10453  axcclem  10459  ttukeylem6  10516  wunex2  10747  wuncval2  10756  intgru  10823  wfgru  10825  qexALT  13013  seqexw  14081  shftfval  15143  vdwapval  17065  restfn  17509  prdsvallem  17539  prdsval  17540  wunfunc  17990  wunnat  18048  arwval  18132  catcfuccl  18207  catcxpccl  18295  yon11  18352  yon12  18353  yon2  18354  yonpropd  18356  oppcyon  18357  yonffth  18372  yoniso  18373  plusffval  18736  grpsubfval  19107  mulgfval  19192  sylow1lem2  19726  sylow2blem1  19747  sylow2blem2  19748  sylow3lem1  19754  sylow3lem6  19759  dmdprd  20127  dprdval  20132  staffval  21007  scaffval  21064  lpival  21555  ipffval  21861  lindsdom  22063  cmpsub  23625  2ndcsep  23685  1stckgen  23780  kgencn2  23783  txcmplem1  23867  blbas  24656  met1stc  24747  psmetutop  24793  nmfval  24814  dchrptlem2  27501  dchrptlem3  27502  mulsproplem9  28389  ishpg  29116  tgplnfn  29132  plngval  29134  isplng  29135  brprlng  29295  edgval  29506  bafval  31085  vsfval  31114  foresf1o  32979  fnpreimac  33143  nsgmgc  33841  nsgqusf1o  33845  idlsrgtset  33918  locfinreflem  34350  cmpcref  34360  rspectopn  34377  ordtconnlem1  34434  qqhval  34482  sigapildsys  34673  dya2icoseg2  34789  dya2iocuni  34794  sxbrsigalem2  34797  sxbrsigalem5  34799  omssubadd  34811  mvtval  36079  mvrsval  36084  mstaval  36123  brrestrict  36528  relowlssretop  38117  exrecfnlem  38133  ctbssinf  38160  indexdom  38484  heiborlem1  38561  isdrngo2  38708  isrngohom  38715  idlval  38763  isidl  38764  igenval  38811  lsatset  39863  dicval  42049  aks6d1c6isolem2  43041  prjcrvfval  43477  trclexi  44460  rtrclexi  44461  dfrtrcl5  44469  dfrcl2  44514  wfaxrep  45817  stoweidlem59  46887  fourierdlem71  47005  salgensscntex  47172  aacllem  50772