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

Theorem rnex 5124
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 5122 . 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 1725   _Vcvv 2948   ran crn 4870
This theorem is referenced by:  elxp4  5348  elxp5  5349  ffoss  5698  fvclex  5972  abrexex  5974  wemoiso2  6070  2ndval  6343  fo2nd  6358  ixpsnf1o  7093  bren  7108  mapen  7262  ssenen  7272  sucdom2  7294  fodomfib  7377  hartogslem1  7500  brwdom  7524  unxpwdom2  7545  noinfep  7603  r0weon  7883  fseqen  7897  acnlem  7918  infpwfien  7932  aceq3lem  7990  dfac4  7992  dfac5  7998  dfac2  8000  dfac9  8005  dfac12lem2  8013  dfac12lem3  8014  infmap2  8087  cfflb  8128  infpssr  8177  fin23lem14  8202  fin23lem16  8204  fin23lem17  8207  fin23lem38  8218  fin23lem39  8219  axdc2lem  8317  axdc3lem2  8320  axcclem  8326  ttukeylem6  8383  wunex2  8602  wuncval2  8611  intgru  8678  wfgru  8680  qexALT  10578  hashfacen  11691  ccatfn  11729  shftfval  11873  vdwapval  13329  restfn  13640  prdsval  13666  wunfunc  14084  wunnat  14141  arwval  14186  catcfuccl  14252  catcxpccl  14292  yon11  14349  yon12  14350  yon2  14351  yonpropd  14353  oppcyon  14354  yonffth  14369  yoniso  14370  plusffval  14690  sylow1lem2  15221  sylow2blem1  15242  sylow2blem2  15243  sylow3lem1  15249  sylow3lem6  15254  dmdprd  15547  dprdval  15549  staffval  15923  scaffval  15956  lpival  16304  ipffval  16867  cmpsub  17451  bwth  17461  2ndcsep  17510  1stckgen  17574  kgencn2  17577  txcmplem1  17661  blbas  18448  met1stc  18539  metutopOLD  18600  psmetutop  18601  nmfval  18624  qtopbaslem  18780  dchrptlem2  21037  dchrptlem3  21038  bafval  22071  vsfval  22102  qqhval  24346  dya2icoseg2  24616  dya2iocuni  24621  sxbrsigalem2  24624  sxbrsigalem5  24626  trpredex  25495  brrestrict  25744  indexdom  26373  heiborlem1  26457  isdrngo2  26511  isrngohom  26518  idlval  26560  isidl  26561  igenval  26608  stoweidlem59  27722  lsatset  29627  dicval  31813
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pr 4395  ax-un 4692
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-rex 2703  df-rab 2706  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-opab 4259  df-cnv 4877  df-dm 4879  df-rn 4880
  Copyright terms: Public domain W3C validator