Theorem rnex 7913

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

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3457  ran crn 5664

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 2148  ax-9 2156  ax-ext 2737  ax-sep 5259  ax-pr 5406  ax-un 7742

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 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-cnv 5671  df-dm 5673  df-rn 5674

This theorem is used by:  elxp4  7925  elxp5  7926  ffoss  7949  fvclex  7962  wemoiso2  7977  2ndval  7995  fo2nd  8013  mapfoss  8855  ixpsnf1o  8942  bren  8959  mapen  9136  ssenen  9146  sucdom2  9194  fodomfib  9295  hartogslem1  9511  brwdom  9536  unxpwdom2  9557  noinfep  9636  r0weon  10012  fseqen  10027  acnlem  10048  infpwfien  10062  aceq3lem  10120  dfac4  10122  dfac5  10128  dfac2b  10130  dfac9  10136  dfac12lem2  10144  dfac12lem3  10145  infmap2  10216  cfflb  10258  infpssr  10307  fin23lem14  10332  fin23lem16  10334  fin23lem17  10337  fin23lem38  10348  fin23lem39  10349  axdc2lem  10447  axdc3lem2  10450  axcclem  10456  ttukeylem6  10513  wunex2  10738  wuncval2  10747  intgru  10814  wfgru  10816  qexALT  13004  seqexw  14071  shftfval  15131  vdwapval  17055  restfn  17499  prdsvallem  17529  prdsval  17530  wunfunc  17980  wunnat  18038  arwval  18122  catcfuccl  18197  catcxpccl  18285  yon11  18342  yon12  18343  yon2  18344  yonpropd  18346  oppcyon  18347  yonffth  18362  yoniso  18363  plusffval  18726  grpsubfval  19094  mulgfval  19179  sylow1lem2  19713  sylow2blem1  19734  sylow2blem2  19735  sylow3lem1  19741  sylow3lem6  19746  dmdprd  20114  dprdval  20119  staffval  20994  scaffval  21051  lpival  21542  ipffval  21848  cmpsub  23607  2ndcsep  23667  1stckgen  23762  kgencn2  23765  txcmplem1  23849  blbas  24638  met1stc  24729  psmetutop  24775  nmfval  24796  dchrptlem2  27480  dchrptlem3  27481  mulsproplem9  28368  ishpg  29092  tgplnfn  29108  plngval  29110  isplng  29111  brprlng  29243  edgval  29454  bafval  31027  vsfval  31056  foresf1o  32921  fnpreimac  33086  nsgmgc  33785  nsgqusf1o  33789  idlsrgtset  33862  locfinreflem  34294  cmpcref  34304  rspectopn  34321  ordtconnlem1  34378  qqhval  34426  sigapildsys  34617  dya2icoseg2  34733  dya2iocuni  34738  sxbrsigalem2  34741  sxbrsigalem5  34743  omssubadd  34755  mvtval  36029  mvrsval  36034  mstaval  36073  brrestrict  36478  relowlssretop  38066  exrecfnlem  38082  ctbssinf  38109  lindsdom  38322  indexdom  38443  heiborlem1  38520  isdrngo2  38667  isrngohom  38674  idlval  38722  isidl  38723  igenval  38770  lsatset  39822  dicval  42008  aks6d1c6isolem2  43000  prjcrvfval  43421  trclexi  44404  rtrclexi  44405  dfrtrcl5  44413  dfrcl2  44458  wfaxrep  45761  stoweidlem59  46831  fourierdlem71  46949  salgensscntex  47116  aacllem  50678