Theorem rnex 7840

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

Syntax hints:   ∈ wcel 2111  Vcvv 3436  ran crn 5615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368  ax-un 7668

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-cnv 5622  df-dm 5624  df-rn 5625

This theorem is referenced by:  elxp4  7852  elxp5  7853  ffoss  7878  fvclex  7891  wemoiso2  7906  2ndval  7924  fo2nd  7942  mapfoss  8776  ixpsnf1o  8862  bren  8879  mapen  9054  ssenen  9064  sucdom2  9112  fodomfib  9213  fodomfibOLD  9215  hartogslem1  9428  brwdom  9453  unxpwdom2  9474  noinfep  9550  r0weon  9903  fseqen  9918  acnlem  9939  infpwfien  9953  aceq3lem  10011  dfac4  10013  dfac5  10020  dfac2b  10022  dfac9  10028  dfac12lem2  10036  dfac12lem3  10037  infmap2  10108  cfflb  10150  infpssr  10199  fin23lem14  10224  fin23lem16  10226  fin23lem17  10229  fin23lem38  10240  fin23lem39  10241  axdc2lem  10339  axdc3lem2  10342  axcclem  10348  ttukeylem6  10405  wunex2  10629  wuncval2  10638  intgru  10705  wfgru  10707  qexALT  12862  seqexw  13924  shftfval  14977  vdwapval  16885  restfn  17328  prdsvallem  17358  prdsval  17359  wunfunc  17808  wunnat  17866  arwval  17950  catcfuccl  18025  catcxpccl  18113  yon11  18170  yon12  18171  yon2  18172  yonpropd  18174  oppcyon  18175  yonffth  18190  yoniso  18191  plusffval  18554  grpsubfval  18896  mulgfval  18982  sylow1lem2  19511  sylow2blem1  19532  sylow2blem2  19533  sylow3lem1  19539  sylow3lem6  19544  dmdprd  19912  dprdval  19917  staffval  20756  scaffval  20813  lpival  21261  ipffval  21585  cmpsub  23315  2ndcsep  23374  1stckgen  23469  kgencn2  23472  txcmplem1  23556  blbas  24345  met1stc  24436  psmetutop  24482  nmfval  24503  dchrptlem2  27203  dchrptlem3  27204  mulsproplem9  28063  ishpg  28737  edgval  29027  bafval  30584  vsfval  30613  foresf1o  32484  fnpreimac  32653  nsgmgc  33377  nsgqusf1o  33381  idlsrgtset  33473  locfinreflem  33853  cmpcref  33863  rspectopn  33880  ordtconnlem1  33937  qqhval  33985  sigapildsys  34175  dya2icoseg2  34291  dya2iocuni  34296  sxbrsigalem2  34299  sxbrsigalem5  34301  omssubadd  34313  mvtval  35544  mvrsval  35549  mstaval  35588  brrestrict  35993  relowlssretop  37407  exrecfnlem  37423  ctbssinf  37450  lindsdom  37653  indexdom  37773  heiborlem1  37850  isdrngo2  37997  isrngohom  38004  idlval  38052  isidl  38053  igenval  38100  lsatset  39088  dicval  41274  aks6d1c6isolem2  42267  prjcrvfval  42723  trclexi  43712  rtrclexi  43713  dfrtrcl5  43721  dfrcl2  43766  wfaxrep  45086  stoweidlem59  46156  fourierdlem71  46274  salgensscntex  46441  aacllem  49901