Theorem rnex 7950

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

Syntax hints:   ∈ wcel 2108  Vcvv 3488  ran crn 5701

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447  ax-un 7770

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-cnv 5708  df-dm 5710  df-rn 5711

This theorem is referenced by:  elxp4  7962  elxp5  7963  ffoss  7986  fvclex  7999  wemoiso2  8015  2ndval  8033  fo2nd  8051  mapfoss  8910  ixpsnf1o  8996  bren  9013  brenOLD  9014  sucdom2OLD  9148  mapen  9207  ssenen  9217  sucdom2  9269  fodomfib  9397  fodomfibOLD  9399  hartogslem1  9611  brwdom  9636  unxpwdom2  9657  noinfep  9729  r0weon  10081  fseqen  10096  acnlem  10117  infpwfien  10131  aceq3lem  10189  dfac4  10191  dfac5  10198  dfac2b  10200  dfac9  10206  dfac12lem2  10214  dfac12lem3  10215  infmap2  10286  cfflb  10328  infpssr  10377  fin23lem14  10402  fin23lem16  10404  fin23lem17  10407  fin23lem38  10418  fin23lem39  10419  axdc2lem  10517  axdc3lem2  10520  axcclem  10526  ttukeylem6  10583  wunex2  10807  wuncval2  10816  intgru  10883  wfgru  10885  qexALT  13029  seqexw  14068  shftfval  15119  vdwapval  17020  restfn  17484  prdsvallem  17514  prdsval  17515  wunfunc  17965  wunfuncOLD  17966  wunnat  18024  wunnatOLD  18025  arwval  18110  catcfuccl  18186  catcfucclOLD  18187  catcxpccl  18276  catcxpcclOLD  18277  yon11  18334  yon12  18335  yon2  18336  yonpropd  18338  oppcyon  18339  yonffth  18354  yoniso  18355  plusffval  18684  grpsubfval  19023  mulgfval  19109  sylow1lem2  19641  sylow2blem1  19662  sylow2blem2  19663  sylow3lem1  19669  sylow3lem6  19674  dmdprd  20042  dprdval  20047  staffval  20864  scaffval  20900  lpival  21357  ipffval  21689  cmpsub  23429  2ndcsep  23488  1stckgen  23583  kgencn2  23586  txcmplem1  23670  blbas  24461  met1stc  24555  psmetutop  24601  nmfval  24622  dchrptlem2  27327  dchrptlem3  27328  mulsproplem9  28168  ishpg  28785  edgval  29084  bafval  30636  vsfval  30665  foresf1o  32532  fnpreimac  32689  nsgmgc  33405  nsgqusf1o  33409  idlsrgtset  33501  locfinreflem  33786  cmpcref  33796  rspectopn  33813  ordtconnlem1  33870  qqhval  33920  sigapildsys  34126  dya2icoseg2  34243  dya2iocuni  34248  sxbrsigalem2  34251  sxbrsigalem5  34253  omssubadd  34265  mvtval  35468  mvrsval  35473  mstaval  35512  brrestrict  35913  relowlssretop  37329  exrecfnlem  37345  ctbssinf  37372  lindsdom  37574  indexdom  37694  heiborlem1  37771  isdrngo2  37918  isrngohom  37925  idlval  37973  isidl  37974  igenval  38021  lsatset  38946  dicval  41133  aks6d1c6isolem2  42132  prjcrvfval  42586  trclexi  43582  rtrclexi  43583  dfrtrcl5  43591  dfrcl2  43636  stoweidlem59  45980  fourierdlem71  46098  salgensscntex  46265  aacllem  48895