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

Theorem rnex 4916
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 4914 . 2  |-  ( A  e.  _V  ->  ran  A  e.  _V )
31, 2ax-mp 10 1  |-  ran  A  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1621   _Vcvv 2757   ran crn 4648
This theorem is referenced by:  elxp4  5133  elxp5  5134  ffoss  5429  fvclex  5681  abrexex  5683  wemoiso2  5776  2ndval  6045  fo2nd  6060  ixpsnf1o  6810  bren  6825  mapen  6979  ssenen  6989  sucdom2  7011  fodomfib  7090  hartogslem1  7211  brwdom  7235  unxpwdom2  7256  noinfep  7314  r0weon  7594  fseqen  7608  acnlem  7629  infpwfien  7643  aceq3lem  7701  dfac4  7703  dfac5  7709  dfac2  7711  dfac9  7716  dfac12lem2  7724  dfac12lem3  7725  infmap2  7798  cfflb  7839  infpssr  7888  fin23lem14  7913  fin23lem16  7915  fin23lem17  7918  fin23lem38  7929  fin23lem39  7930  axdc2lem  8028  axdc3lem2  8031  axcclem  8037  ttukeylem6  8095  wunex2  8314  wuncval2  8323  intgru  8390  wfgru  8392  qexALT  10284  hashfacen  11343  ccatfn  11378  shftfval  11516  vdwapval  12968  restfn  13277  prdsval  13303  wunfunc  13721  wunnat  13778  arwval  13823  catcfuccl  13889  catcxpccl  13929  yon11  13986  yon12  13987  yon2  13988  yonpropd  13990  oppcyon  13991  yonffth  14006  yoniso  14007  plusffval  14327  sylow1lem2  14858  sylow2blem1  14879  sylow2blem2  14880  sylow3lem1  14886  sylow3lem6  14891  dmdprd  15184  dprdval  15186  staffval  15560  scaffval  15593  lpival  15945  ipffval  16500  cmpsub  17075  2ndcsep  17133  1stckgen  17197  kgencn2  17200  txcmplem1  17283  blbas  17924  met1stc  18015  nmfval  18059  qtopbaslem  18215  dchrptlem2  20452  dchrptlem3  20453  bafval  21106  vsfval  21137  trpredex  23595  brrestrict  23848  svli2  24837  svs2  24840  basexre  24875  bwt2  24945  indexdom  25766  heiborlem1  25888  isdrngo2  25942  isrngohom  25949  idlval  25991  isidl  25992  igenval  26039  stoweidlem59  27129  lsatset  28331  dicval  30517
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-sep 4101  ax-nul 4109  ax-pr 4172  ax-un 4470
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2121  df-mo 2122  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-rex 2522  df-rab 2525  df-v 2759  df-dif 3116  df-un 3118  df-in 3120  df-ss 3127  df-nul 3417  df-if 3526  df-sn 3606  df-pr 3607  df-op 3609  df-uni 3788  df-br 3984  df-opab 4038  df-cnv 4663  df-dm 4665  df-rn 4666
  Copyright terms: Public domain W3C validator