Theorem rnex 7866

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

Syntax hints:   ∈ wcel 2109  Vcvv 3444  ran crn 5632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382  ax-un 7691

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-cnv 5639  df-dm 5641  df-rn 5642

This theorem is referenced by:  elxp4  7878  elxp5  7879  ffoss  7904  fvclex  7917  wemoiso2  7932  2ndval  7950  fo2nd  7968  mapfoss  8802  ixpsnf1o  8888  bren  8905  mapen  9082  ssenen  9092  sucdom2  9144  fodomfib  9256  fodomfibOLD  9258  hartogslem1  9471  brwdom  9496  unxpwdom2  9517  noinfep  9589  r0weon  9941  fseqen  9956  acnlem  9977  infpwfien  9991  aceq3lem  10049  dfac4  10051  dfac5  10058  dfac2b  10060  dfac9  10066  dfac12lem2  10074  dfac12lem3  10075  infmap2  10146  cfflb  10188  infpssr  10237  fin23lem14  10262  fin23lem16  10264  fin23lem17  10267  fin23lem38  10278  fin23lem39  10279  axdc2lem  10377  axdc3lem2  10380  axcclem  10386  ttukeylem6  10443  wunex2  10667  wuncval2  10676  intgru  10743  wfgru  10745  qexALT  12899  seqexw  13958  shftfval  15012  vdwapval  16920  restfn  17363  prdsvallem  17393  prdsval  17394  wunfunc  17839  wunnat  17897  arwval  17981  catcfuccl  18056  catcxpccl  18144  yon11  18201  yon12  18202  yon2  18203  yonpropd  18205  oppcyon  18206  yonffth  18221  yoniso  18222  plusffval  18549  grpsubfval  18891  mulgfval  18977  sylow1lem2  19505  sylow2blem1  19526  sylow2blem2  19527  sylow3lem1  19533  sylow3lem6  19538  dmdprd  19906  dprdval  19911  staffval  20726  scaffval  20762  lpival  21210  ipffval  21533  cmpsub  23263  2ndcsep  23322  1stckgen  23417  kgencn2  23420  txcmplem1  23504  blbas  24294  met1stc  24385  psmetutop  24431  nmfval  24452  dchrptlem2  27152  dchrptlem3  27153  mulsproplem9  28003  ishpg  28662  edgval  28952  bafval  30506  vsfval  30535  foresf1o  32406  fnpreimac  32568  nsgmgc  33356  nsgqusf1o  33360  idlsrgtset  33452  locfinreflem  33803  cmpcref  33813  rspectopn  33830  ordtconnlem1  33887  qqhval  33935  sigapildsys  34125  dya2icoseg2  34242  dya2iocuni  34247  sxbrsigalem2  34250  sxbrsigalem5  34252  omssubadd  34264  mvtval  35460  mvrsval  35465  mstaval  35504  brrestrict  35910  relowlssretop  37324  exrecfnlem  37340  ctbssinf  37367  lindsdom  37581  indexdom  37701  heiborlem1  37778  isdrngo2  37925  isrngohom  37932  idlval  37980  isidl  37981  igenval  38028  lsatset  38956  dicval  41143  aks6d1c6isolem2  42136  prjcrvfval  42592  trclexi  43582  rtrclexi  43583  dfrtrcl5  43591  dfrcl2  43636  wfaxrep  44957  stoweidlem59  46030  fourierdlem71  46148  salgensscntex  46315  aacllem  49763