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

Theorem rnex 5092
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 5090 . 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 1721   _Vcvv 2916   ran crn 4838
This theorem is referenced by:  elxp4  5316  elxp5  5317  ffoss  5666  fvclex  5940  abrexex  5942  wemoiso2  6038  2ndval  6311  fo2nd  6326  ixpsnf1o  7061  bren  7076  mapen  7230  ssenen  7240  sucdom2  7262  fodomfib  7345  hartogslem1  7467  brwdom  7491  unxpwdom2  7512  noinfep  7570  r0weon  7850  fseqen  7864  acnlem  7885  infpwfien  7899  aceq3lem  7957  dfac4  7959  dfac5  7965  dfac2  7967  dfac9  7972  dfac12lem2  7980  dfac12lem3  7981  infmap2  8054  cfflb  8095  infpssr  8144  fin23lem14  8169  fin23lem16  8171  fin23lem17  8174  fin23lem38  8185  fin23lem39  8186  axdc2lem  8284  axdc3lem2  8287  axcclem  8293  ttukeylem6  8350  wunex2  8569  wuncval2  8578  intgru  8645  wfgru  8647  qexALT  10545  hashfacen  11658  ccatfn  11696  shftfval  11840  vdwapval  13296  restfn  13607  prdsval  13633  wunfunc  14051  wunnat  14108  arwval  14153  catcfuccl  14219  catcxpccl  14259  yon11  14316  yon12  14317  yon2  14318  yonpropd  14320  oppcyon  14321  yonffth  14336  yoniso  14337  plusffval  14657  sylow1lem2  15188  sylow2blem1  15209  sylow2blem2  15210  sylow3lem1  15216  sylow3lem6  15221  dmdprd  15514  dprdval  15516  staffval  15890  scaffval  15923  lpival  16271  ipffval  16834  cmpsub  17417  2ndcsep  17475  1stckgen  17539  kgencn2  17542  txcmplem1  17626  blbas  18413  met1stc  18504  metutopOLD  18565  psmetutop  18566  nmfval  18589  qtopbaslem  18745  dchrptlem2  21002  dchrptlem3  21003  bafval  22036  vsfval  22067  qqhval  24311  dya2icoseg2  24581  dya2iocuni  24586  sxbrsigalem2  24589  sxbrsigalem5  24591  trpredex  25454  brrestrict  25702  indexdom  26326  heiborlem1  26410  isdrngo2  26464  isrngohom  26471  idlval  26513  isidl  26514  igenval  26561  stoweidlem59  27675  lsatset  29473  dicval  31659
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363  ax-un 4660
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2258  df-mo 2259  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-rex 2672  df-rab 2675  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783  df-uni 3976  df-br 4173  df-opab 4227  df-cnv 4845  df-dm 4847  df-rn 4848
  Copyright terms: Public domain W3C validator