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

Theorem rnex 4895
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 4893 . 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 2740   ran crn 4627
This theorem is referenced by:  elxp4  5112  elxp5  5113  ffoss  5408  fvclex  5660  abrexex  5662  wemoiso2  5755  2ndval  6024  fo2nd  6039  ixpsnf1o  6789  bren  6804  mapen  6958  ssenen  6968  sucdom2  6990  fodomfib  7069  hartogslem1  7190  brwdom  7214  unxpwdom2  7235  noinfep  7293  r0weon  7573  fseqen  7587  acnlem  7608  infpwfien  7622  aceq3lem  7680  dfac4  7682  dfac5  7688  dfac2  7690  dfac9  7695  dfac12lem2  7703  dfac12lem3  7704  infmap2  7777  cfflb  7818  infpssr  7867  fin23lem14  7892  fin23lem16  7894  fin23lem17  7897  fin23lem38  7908  fin23lem39  7909  axdc2lem  8007  axdc3lem2  8010  axcclem  8016  ttukeylem6  8074  wunex2  8293  wuncval2  8302  intgru  8369  wfgru  8371  qexALT  10263  hashfacen  11322  ccatfn  11357  shftfval  11495  vdwapval  12947  restfn  13256  prdsval  13282  wunfunc  13700  wunnat  13757  arwval  13802  catcfuccl  13868  catcxpccl  13908  yon11  13965  yon12  13966  yon2  13967  yonpropd  13969  oppcyon  13970  yonffth  13985  yoniso  13986  plusffval  14306  sylow1lem2  14837  sylow2blem1  14858  sylow2blem2  14859  sylow3lem1  14865  sylow3lem6  14870  dmdprd  15163  dprdval  15165  staffval  15539  scaffval  15572  lpival  15924  ipffval  16479  cmpsub  17054  2ndcsep  17112  1stckgen  17176  kgencn2  17179  txcmplem1  17262  blbas  17903  met1stc  17994  nmfval  18038  qtopbaslem  18194  dchrptlem2  20431  dchrptlem3  20432  bafval  21085  vsfval  21116  trpredex  23574  brrestrict  23827  svli2  24816  svs2  24819  basexre  24854  bwt2  24924  indexdom  25745  heiborlem1  25867  isdrngo2  25921  isrngohom  25928  idlval  25970  isidl  25971  igenval  26018  stoweidlem59  27108  lsatset  28310  dicval  30496
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 4081  ax-nul 4089  ax-pr 4152  ax-un 4449
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 2521  df-rab 2523  df-v 2742  df-dif 3097  df-un 3099  df-in 3101  df-ss 3108  df-nul 3398  df-if 3507  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3769  df-br 3964  df-opab 4018  df-cnv 4642  df-dm 4644  df-rn 4645
  Copyright terms: Public domain W3C validator