Theorem rnex 7916

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

This proof depends on syntax axioms:   ∈ wcel 2146  Vcvv 3458  ran crn 5667

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 2738  ax-sep 5262  ax-pr 5409  ax-un 7745

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 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-cnv 5674  df-dm 5676  df-rn 5677

This theorem is used by:  elxp4  7928  elxp5  7929  ffoss  7952  fvclex  7965  wemoiso2  7980  2ndval  7998  fo2nd  8016  mapfoss  8858  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  10741  wuncval2  10750  intgru  10817  wfgru  10819  qexALT  13006  seqexw  14073  shftfval  15133  vdwapval  17058  restfn  17502  prdsvallem  17532  prdsval  17533  wunfunc  17983  wunnat  18041  arwval  18125  catcfuccl  18200  catcxpccl  18288  yon11  18345  yon12  18346  yon2  18347  yonpropd  18349  oppcyon  18350  yonffth  18365  yoniso  18366  plusffval  18729  grpsubfval  19075  mulgfval  19160  sylow1lem2  19694  sylow2blem1  19715  sylow2blem2  19716  sylow3lem1  19722  sylow3lem6  19727  dmdprd  20095  dprdval  20100  staffval  20974  scaffval  21031  lpival  21522  ipffval  21828  cmpsub  23587  2ndcsep  23646  1stckgen  23741  kgencn2  23744  txcmplem1  23828  blbas  24617  met1stc  24708  psmetutop  24754  nmfval  24775  dchrptlem2  27459  dchrptlem3  27460  mulsproplem9  28347  ishpg  29071  tgplnfn  29087  plngval  29089  isplng  29090  brprlng  29218  edgval  29429  bafval  30986  vsfval  31015  foresf1o  32880  fnpreimac  33045  nsgmgc  33745  nsgqusf1o  33749  idlsrgtset  33822  locfinreflem  34254  cmpcref  34264  rspectopn  34281  ordtconnlem1  34338  qqhval  34386  sigapildsys  34576  dya2icoseg2  34692  dya2iocuni  34697  sxbrsigalem2  34700  sxbrsigalem5  34702  omssubadd  34714  mvtval  36005  mvrsval  36010  mstaval  36049  brrestrict  36454  relowlssretop  38042  exrecfnlem  38058  ctbssinf  38085  lindsdom  38298  indexdom  38418  heiborlem1  38495  isdrngo2  38642  isrngohom  38649  idlval  38697  isidl  38698  igenval  38745  lsatset  39797  dicval  41983  aks6d1c6isolem2  42975  prjcrvfval  43396  trclexi  44379  rtrclexi  44380  dfrtrcl5  44388  dfrcl2  44433  wfaxrep  45736  stoweidlem59  46806  fourierdlem71  46924  salgensscntex  47091  aacllem  50654