Theorem rnex 7861

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

Syntax hints:   ∈ wcel 2114  Vcvv 3429  ran crn 5632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-cnv 5639  df-dm 5641  df-rn 5642

This theorem is referenced by:  elxp4  7873  elxp5  7874  ffoss  7899  fvclex  7912  wemoiso2  7927  2ndval  7945  fo2nd  7963  mapfoss  8799  ixpsnf1o  8886  bren  8903  mapen  9079  ssenen  9089  sucdom2  9137  fodomfib  9239  fodomfibOLD  9241  hartogslem1  9457  brwdom  9482  unxpwdom2  9503  noinfep  9581  r0weon  9934  fseqen  9949  acnlem  9970  infpwfien  9984  aceq3lem  10042  dfac4  10044  dfac5  10051  dfac2b  10053  dfac9  10059  dfac12lem2  10067  dfac12lem3  10068  infmap2  10139  cfflb  10181  infpssr  10230  fin23lem14  10255  fin23lem16  10257  fin23lem17  10260  fin23lem38  10271  fin23lem39  10272  axdc2lem  10370  axdc3lem2  10373  axcclem  10379  ttukeylem6  10436  wunex2  10661  wuncval2  10670  intgru  10737  wfgru  10739  qexALT  12914  seqexw  13979  shftfval  15032  vdwapval  16944  restfn  17387  prdsvallem  17417  prdsval  17418  wunfunc  17868  wunnat  17926  arwval  18010  catcfuccl  18085  catcxpccl  18173  yon11  18230  yon12  18231  yon2  18232  yonpropd  18234  oppcyon  18235  yonffth  18250  yoniso  18251  plusffval  18614  grpsubfval  18959  mulgfval  19045  sylow1lem2  19574  sylow2blem1  19595  sylow2blem2  19596  sylow3lem1  19602  sylow3lem6  19607  dmdprd  19975  dprdval  19980  staffval  20818  scaffval  20875  lpival  21322  ipffval  21628  cmpsub  23365  2ndcsep  23424  1stckgen  23519  kgencn2  23522  txcmplem1  23606  blbas  24395  met1stc  24486  psmetutop  24532  nmfval  24553  dchrptlem2  27228  dchrptlem3  27229  mulsproplem9  28116  ishpg  28827  edgval  29118  bafval  30675  vsfval  30704  foresf1o  32574  fnpreimac  32743  nsgmgc  33472  nsgqusf1o  33476  idlsrgtset  33568  locfinreflem  33984  cmpcref  33994  rspectopn  34011  ordtconnlem1  34068  qqhval  34116  sigapildsys  34306  dya2icoseg2  34422  dya2iocuni  34427  sxbrsigalem2  34430  sxbrsigalem5  34432  omssubadd  34444  mvtval  35682  mvrsval  35687  mstaval  35726  brrestrict  36131  relowlssretop  37679  exrecfnlem  37695  ctbssinf  37722  lindsdom  37935  indexdom  38055  heiborlem1  38132  isdrngo2  38279  isrngohom  38286  idlval  38334  isidl  38335  igenval  38382  lsatset  39436  dicval  41622  aks6d1c6isolem2  42614  prjcrvfval  43064  trclexi  44047  rtrclexi  44048  dfrtrcl5  44056  dfrcl2  44101  wfaxrep  45421  stoweidlem59  46487  fourierdlem71  46605  salgensscntex  46772  aacllem  50276