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

Theorem rnex 6741
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 6739 . 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 1872   _Vcvv 3080   ran crn 4854
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546  ax-nul 4555  ax-pr 4660  ax-un 6597
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-rex 2777  df-rab 2780  df-v 3082  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3912  df-sn 3999  df-pr 4001  df-op 4005  df-uni 4220  df-br 4424  df-opab 4483  df-cnv 4861  df-dm 4863  df-rn 4864
This theorem is referenced by:  elxp4  6751  elxp5  6752  ffoss  6768  fvclex  6779  abrexex  6781  wemoiso2  6793  2ndval  6810  fo2nd  6828  ixpsnf1o  7573  bren  7589  mapen  7745  ssenen  7755  sucdom2  7777  fodomfib  7860  hartogslem1  8066  brwdom  8091  unxpwdom2  8112  noinfep  8173  r0weon  8451  fseqen  8465  acnlem  8486  infpwfien  8500  aceq3lem  8558  dfac4  8560  dfac5  8566  dfac2  8568  dfac9  8573  dfac12lem2  8581  dfac12lem3  8582  infmap2  8655  cfflb  8696  infpssr  8745  fin23lem14  8770  fin23lem16  8772  fin23lem17  8775  fin23lem38  8786  fin23lem39  8787  axdc2lem  8885  axdc3lem2  8888  axcclem  8894  ttukeylem6  8951  wunex2  9170  wuncval2  9179  intgru  9246  wfgru  9248  qexALT  11286  hashfacen  12621  ccatfnOLD  12722  shftfval  13133  vdwapval  14922  restfn  15322  prdsval  15352  wunfunc  15803  wunnat  15860  arwval  15937  catcfuccl  16003  catcxpccl  16091  yon11  16148  yon12  16149  yon2  16150  yonpropd  16152  oppcyon  16153  yonffth  16168  yoniso  16169  plusffval  16492  sylow1lem2  17250  sylow2blem1  17271  sylow2blem2  17272  sylow3lem1  17278  sylow3lem6  17283  dmdprd  17629  dprdval  17634  staffval  18074  scaffval  18108  lpival  18468  ipffval  19213  cmpsub  20413  2ndcsep  20472  1stckgen  20567  kgencn2  20570  txcmplem1  20654  blbas  21443  met1stc  21534  psmetutop  21580  nmfval  21601  qtopbaslem  21777  dchrptlem2  24191  dchrptlem3  24192  ishpg  24799  edgval  25064  bafval  26221  vsfval  26252  foresf1o  28138  locfinreflem  28675  cmpcref  28685  ordtconlem1  28738  qqhval  28786  sigapildsys  28992  dya2icoseg2  29108  dya2iocuni  29113  sxbrsigalem2  29116  sxbrsigalem5  29118  omssubadd  29136  omssubaddOLD  29140  mvtval  30146  mvrsval  30151  mstaval  30190  trpredex  30485  brrestrict  30721  relowlssretop  31730  indexdom  32025  heiborlem1  32107  isdrngo2  32161  isrngohom  32168  idlval  32210  isidl  32211  igenval  32258  lsatset  32525  dicval  34713  trclexi  36197  rtrclexi  36198  dfrtrcl5  36206  dfrcl2  36236  stoweidlem59  37860  fourierdlem71  37981  edgaval  39029  aacllem  40162
  Copyright terms: Public domain W3C validator