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

Theorem rnex 4958
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 4956 . 2  |-  ( A  e.  _V  ->  ran  A  e.  _V )
31, 2ax-mp 8 1  |-  ran  A  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1696   _Vcvv 2801   ran crn 4706
This theorem is referenced by:  elxp4  5176  elxp5  5177  ffoss  5521  fvclex  5777  abrexex  5779  wemoiso2  5872  2ndval  6141  fo2nd  6156  ixpsnf1o  6872  bren  6887  mapen  7041  ssenen  7051  sucdom2  7073  fodomfib  7152  hartogslem1  7273  brwdom  7297  unxpwdom2  7318  noinfep  7376  r0weon  7656  fseqen  7670  acnlem  7691  infpwfien  7705  aceq3lem  7763  dfac4  7765  dfac5  7771  dfac2  7773  dfac9  7778  dfac12lem2  7786  dfac12lem3  7787  infmap2  7860  cfflb  7901  infpssr  7950  fin23lem14  7975  fin23lem16  7977  fin23lem17  7980  fin23lem38  7991  fin23lem39  7992  axdc2lem  8090  axdc3lem2  8093  axcclem  8099  ttukeylem6  8157  wunex2  8376  wuncval2  8385  intgru  8452  wfgru  8454  qexALT  10347  hashfacen  11408  ccatfn  11443  shftfval  11581  vdwapval  13036  restfn  13345  prdsval  13371  wunfunc  13789  wunnat  13846  arwval  13891  catcfuccl  13957  catcxpccl  13997  yon11  14054  yon12  14055  yon2  14056  yonpropd  14058  oppcyon  14059  yonffth  14074  yoniso  14075  plusffval  14395  sylow1lem2  14926  sylow2blem1  14947  sylow2blem2  14948  sylow3lem1  14954  sylow3lem6  14959  dmdprd  15252  dprdval  15254  staffval  15628  scaffval  15661  lpival  16013  ipffval  16568  cmpsub  17143  2ndcsep  17201  1stckgen  17265  kgencn2  17268  txcmplem1  17351  blbas  17992  met1stc  18083  nmfval  18127  qtopbaslem  18283  dchrptlem2  20520  dchrptlem3  20521  bafval  21176  vsfval  21207  dya2iocrfn  23595  dya2iocct  23596  dya2iocrrnval  23597  trpredex  24311  brrestrict  24559  svli2  25587  svs2  25590  basexre  25625  bwt2  25695  indexdom  26516  heiborlem1  26638  isdrngo2  26692  isrngohom  26699  idlval  26741  isidl  26742  igenval  26789  stoweidlem59  27911  lsatset  29802  dicval  31988
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pr 4230  ax-un 4528
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-rex 2562  df-rab 2565  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-opab 4094  df-cnv 4713  df-dm 4715  df-rn 4716
  Copyright terms: Public domain W3C validator