Theorem rnex 7911

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

Syntax hints:   ∈ wcel 2109  Vcvv 3464  ran crn 5660

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 2708  ax-sep 5271  ax-nul 5281  ax-pr 5407  ax-un 7734

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 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-cnv 5667  df-dm 5669  df-rn 5670

This theorem is referenced by:  elxp4  7923  elxp5  7924  ffoss  7949  fvclex  7962  wemoiso2  7978  2ndval  7996  fo2nd  8014  mapfoss  8871  ixpsnf1o  8957  bren  8974  sucdom2OLD  9101  mapen  9160  ssenen  9170  sucdom2  9222  fodomfib  9346  fodomfibOLD  9348  hartogslem1  9561  brwdom  9586  unxpwdom2  9607  noinfep  9679  r0weon  10031  fseqen  10046  acnlem  10067  infpwfien  10081  aceq3lem  10139  dfac4  10141  dfac5  10148  dfac2b  10150  dfac9  10156  dfac12lem2  10164  dfac12lem3  10165  infmap2  10236  cfflb  10278  infpssr  10327  fin23lem14  10352  fin23lem16  10354  fin23lem17  10357  fin23lem38  10368  fin23lem39  10369  axdc2lem  10467  axdc3lem2  10470  axcclem  10476  ttukeylem6  10533  wunex2  10757  wuncval2  10766  intgru  10833  wfgru  10835  qexALT  12985  seqexw  14040  shftfval  15094  vdwapval  16998  restfn  17443  prdsvallem  17473  prdsval  17474  wunfunc  17919  wunnat  17977  arwval  18061  catcfuccl  18136  catcxpccl  18224  yon11  18281  yon12  18282  yon2  18283  yonpropd  18285  oppcyon  18286  yonffth  18301  yoniso  18302  plusffval  18629  grpsubfval  18971  mulgfval  19057  sylow1lem2  19585  sylow2blem1  19606  sylow2blem2  19607  sylow3lem1  19613  sylow3lem6  19618  dmdprd  19986  dprdval  19991  staffval  20806  scaffval  20842  lpival  21290  ipffval  21613  cmpsub  23343  2ndcsep  23402  1stckgen  23497  kgencn2  23500  txcmplem1  23584  blbas  24374  met1stc  24465  psmetutop  24511  nmfval  24532  dchrptlem2  27233  dchrptlem3  27234  mulsproplem9  28084  ishpg  28743  edgval  29033  bafval  30590  vsfval  30619  foresf1o  32490  fnpreimac  32654  nsgmgc  33432  nsgqusf1o  33436  idlsrgtset  33528  locfinreflem  33876  cmpcref  33886  rspectopn  33903  ordtconnlem1  33960  qqhval  34008  sigapildsys  34198  dya2icoseg2  34315  dya2iocuni  34320  sxbrsigalem2  34323  sxbrsigalem5  34325  omssubadd  34337  mvtval  35527  mvrsval  35532  mstaval  35571  brrestrict  35972  relowlssretop  37386  exrecfnlem  37402  ctbssinf  37429  lindsdom  37643  indexdom  37763  heiborlem1  37840  isdrngo2  37987  isrngohom  37994  idlval  38042  isidl  38043  igenval  38090  lsatset  39013  dicval  41200  aks6d1c6isolem2  42193  prjcrvfval  42629  trclexi  43619  rtrclexi  43620  dfrtrcl5  43628  dfrcl2  43673  wfaxrep  44994  stoweidlem59  46068  fourierdlem71  46186  salgensscntex  46353  aacllem  49645