MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rnex Structured version   Unicode version

Theorem rnex 6511
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  |-  A  e. 
_V
Assertion
Ref Expression
rnex  |-  ran  A  e.  _V

Proof of Theorem rnex
StepHypRef Expression
1 dmex.1 . 2  |-  A  e. 
_V
2 rnexg 6509 . 2  |-  ( A  e.  _V  ->  ran  A  e.  _V )
31, 2ax-mp 5 1  |-  ran  A  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1761   _Vcvv 2970   ran crn 4837
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pr 4528  ax-un 6371
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2261  df-mo 2262  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-rex 2719  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-br 4290  df-opab 4348  df-cnv 4844  df-dm 4846  df-rn 4847
This theorem is referenced by:  elxp4  6521  elxp5  6522  ffoss  6537  fvclex  6548  abrexex  6550  wemoiso2  6562  2ndval  6579  fo2nd  6596  ixpsnf1o  7299  bren  7315  mapen  7471  ssenen  7481  sucdom2  7503  fodomfib  7587  hartogslem1  7752  brwdom  7778  unxpwdom2  7799  noinfep  7861  r0weon  8175  fseqen  8193  acnlem  8214  infpwfien  8228  aceq3lem  8286  dfac4  8288  dfac5  8294  dfac2  8296  dfac9  8301  dfac12lem2  8309  dfac12lem3  8310  infmap2  8383  cfflb  8424  infpssr  8473  fin23lem14  8498  fin23lem16  8500  fin23lem17  8503  fin23lem38  8514  fin23lem39  8515  axdc2lem  8613  axdc3lem2  8616  axcclem  8622  ttukeylem6  8679  wunex2  8901  wuncval2  8910  intgru  8977  wfgru  8979  qexALT  10964  hashfacen  12203  ccatfn  12268  shftfval  12555  vdwapval  14030  restfn  14359  prdsval  14389  wunfunc  14805  wunnat  14862  arwval  14907  catcfuccl  14973  catcxpccl  15013  yon11  15070  yon12  15071  yon2  15072  yonpropd  15074  oppcyon  15075  yonffth  15090  yoniso  15091  plusffval  15423  sylow1lem2  16091  sylow2blem1  16112  sylow2blem2  16113  sylow3lem1  16119  sylow3lem6  16124  dmdprd  16470  dprdval  16475  dprdvalOLD  16477  staffval  16912  scaffval  16946  lpival  17305  ipffval  18036  cmpsub  18962  bwthOLD  18973  2ndcsep  19022  1stckgen  19086  kgencn2  19089  txcmplem1  19173  blbas  19964  met1stc  20055  metutopOLD  20116  psmetutop  20117  nmfval  20140  qtopbaslem  20296  dchrptlem2  22563  dchrptlem3  22564  bafval  23917  vsfval  23948  ordtconlem1  26290  qqhval  26339  dya2icoseg2  26629  dya2iocuni  26634  sxbrsigalem2  26637  sxbrsigalem5  26639  trpredex  27630  brrestrict  27909  indexdom  28553  heiborlem1  28635  isdrngo2  28689  isrngohom  28696  idlval  28738  isidl  28739  igenval  28786  stoweidlem59  29779  lsatset  32357  dicval  34543
  Copyright terms: Public domain W3C validator