Theorem rnex 7899

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

Syntax hints:   ∈ wcel 2106  Vcvv 3474  ran crn 5676

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7721

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-cnv 5683  df-dm 5685  df-rn 5686

This theorem is referenced by:  elxp4  7909  elxp5  7910  ffoss  7928  fvclex  7941  wemoiso2  7957  2ndval  7974  fo2nd  7992  mapfoss  8842  ixpsnf1o  8928  bren  8945  brenOLD  8946  sucdom2OLD  9078  mapen  9137  ssenen  9147  sucdom2  9202  fodomfib  9322  hartogslem1  9533  brwdom  9558  unxpwdom2  9579  noinfep  9651  r0weon  10003  fseqen  10018  acnlem  10039  infpwfien  10053  aceq3lem  10111  dfac4  10113  dfac5  10119  dfac2b  10121  dfac9  10127  dfac12lem2  10135  dfac12lem3  10136  infmap2  10209  cfflb  10250  infpssr  10299  fin23lem14  10324  fin23lem16  10326  fin23lem17  10329  fin23lem38  10340  fin23lem39  10341  axdc2lem  10439  axdc3lem2  10442  axcclem  10448  ttukeylem6  10505  wunex2  10729  wuncval2  10738  intgru  10805  wfgru  10807  qexALT  12944  seqexw  13978  hashfacenOLD  14410  shftfval  15013  vdwapval  16902  restfn  17366  prdsvallem  17396  prdsval  17397  wunfunc  17845  wunfuncOLD  17846  wunnat  17903  wunnatOLD  17904  arwval  17989  catcfuccl  18065  catcfucclOLD  18066  catcxpccl  18155  catcxpcclOLD  18156  yon11  18213  yon12  18214  yon2  18215  yonpropd  18217  oppcyon  18218  yonffth  18233  yoniso  18234  plusffval  18563  grpsubfval  18864  mulgfval  18946  sylow1lem2  19461  sylow2blem1  19482  sylow2blem2  19483  sylow3lem1  19489  sylow3lem6  19494  dmdprd  19862  dprdval  19867  staffval  20447  scaffval  20482  lpival  20875  ipffval  21192  cmpsub  22895  2ndcsep  22954  1stckgen  23049  kgencn2  23052  txcmplem1  23136  blbas  23927  met1stc  24021  psmetutop  24067  nmfval  24088  dchrptlem2  26757  dchrptlem3  26758  mulsproplem9  27569  ishpg  27999  edgval  28298  bafval  29844  vsfval  29873  foresf1o  31729  fnpreimac  31883  nsgmgc  32511  nsgqusf1o  32515  idlsrgtset  32610  locfinreflem  32808  cmpcref  32818  rspectopn  32835  ordtconnlem1  32892  qqhval  32942  sigapildsys  33148  dya2icoseg2  33265  dya2iocuni  33270  sxbrsigalem2  33273  sxbrsigalem5  33275  omssubadd  33287  mvtval  34479  mvrsval  34484  mstaval  34523  brrestrict  34909  relowlssretop  36232  exrecfnlem  36248  ctbssinf  36275  lindsdom  36470  indexdom  36590  heiborlem1  36667  isdrngo2  36814  isrngohom  36821  idlval  36869  isidl  36870  igenval  36917  lsatset  37848  dicval  40035  prjcrvfval  41369  trclexi  42356  rtrclexi  42357  dfrtrcl5  42365  dfrcl2  42410  stoweidlem59  44761  fourierdlem71  44879  salgensscntex  45046  aacllem  47801