Theorem rnex 7599

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

Syntax hints:   ∈ wcel 2111  Vcvv 3441  ran crn 5520

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-cnv 5527  df-dm 5529  df-rn 5530

This theorem is referenced by:  elxp4  7609  elxp5  7610  ffoss  7629  fvclex  7642  wemoiso2  7657  2ndval  7674  fo2nd  7692  ixpsnf1o  8485  bren  8501  sucdom2  8610  mapen  8665  ssenen  8675  fodomfib  8782  hartogslem1  8990  brwdom  9015  unxpwdom2  9036  noinfep  9107  r0weon  9423  fseqen  9438  acnlem  9459  infpwfien  9473  aceq3lem  9531  dfac4  9533  dfac5  9539  dfac2b  9541  dfac9  9547  dfac12lem2  9555  dfac12lem3  9556  infmap2  9629  cfflb  9670  infpssr  9719  fin23lem14  9744  fin23lem16  9746  fin23lem17  9749  fin23lem38  9760  fin23lem39  9761  axdc2lem  9859  axdc3lem2  9862  axcclem  9868  ttukeylem6  9925  wunex2  10149  wuncval2  10158  intgru  10225  wfgru  10227  qexALT  12351  seqexw  13380  hashfacen  13808  shftfval  14421  vdwapval  16299  restfn  16690  prdsval  16720  wunfunc  17161  wunnat  17218  arwval  17295  catcfuccl  17361  catcxpccl  17449  yon11  17506  yon12  17507  yon2  17508  yonpropd  17510  oppcyon  17511  yonffth  17526  yoniso  17527  plusffval  17850  grpsubfval  18139  mulgfval  18218  sylow1lem2  18716  sylow2blem1  18737  sylow2blem2  18738  sylow3lem1  18744  sylow3lem6  18749  dmdprd  19113  dprdval  19118  staffval  19611  scaffval  19645  lpival  20011  ipffval  20337  cmpsub  22005  2ndcsep  22064  1stckgen  22159  kgencn2  22162  txcmplem1  22246  blbas  23037  met1stc  23128  psmetutop  23174  nmfval  23195  dchrptlem2  25849  dchrptlem3  25850  ishpg  26553  edgval  26842  bafval  28387  vsfval  28416  foresf1o  30273  fnpreimac  30434  idlsrgtset  31061  locfinreflem  31193  cmpcref  31203  rspectopn  31220  ordtconnlem1  31277  qqhval  31325  sigapildsys  31531  dya2icoseg2  31646  dya2iocuni  31651  sxbrsigalem2  31654  sxbrsigalem5  31656  omssubadd  31668  mvtval  32860  mvrsval  32865  mstaval  32904  trpredex  33189  brrestrict  33523  relowlssretop  34780  exrecfnlem  34796  ctbssinf  34823  lindsdom  35051  indexdom  35172  heiborlem1  35249  isdrngo2  35396  isrngohom  35403  idlval  35451  isidl  35452  igenval  35499  lsatset  36286  dicval  38472  trclexi  40320  rtrclexi  40321  dfrtrcl5  40329  dfrcl2  40375  stoweidlem59  42701  fourierdlem71  42819  salgensscntex  42984  aacllem  45329