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

Theorem rnex 4849
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 4847 . 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 2727   ran crn 4581
This theorem is referenced by:  elxp4  5066  elxp5  5067  ffoss  5362  fvclex  5613  abrexex  5615  wemoiso2  5708  2ndval  5977  fo2nd  5992  ixpsnf1o  6742  bren  6757  mapen  6910  ssenen  6920  sucdom2  6942  fodomfib  7021  hartogslem1  7141  brwdom  7165  unxpwdom2  7186  noinfep  7244  r0weon  7524  fseqen  7538  acnlem  7559  infpwfien  7573  aceq3lem  7631  dfac4  7633  dfac5  7639  dfac2  7641  dfac9  7646  dfac12lem2  7654  dfac12lem3  7655  infmap2  7728  cfflb  7769  infpssr  7818  fin23lem14  7843  fin23lem16  7845  fin23lem17  7848  fin23lem38  7859  fin23lem39  7860  axdc2lem  7958  axdc3lem2  7961  axcclem  7967  ttukeylem6  8025  wunex2  8240  wuncval2  8249  intgru  8316  wfgru  8318  qexALT  10210  hashfacen  11269  ccatfn  11304  shftfval  11442  vdwapval  12894  restfn  13203  prdsval  13229  wunfunc  13617  wunnat  13674  arwval  13719  catcfuccl  13785  catcxpccl  13825  yon11  13882  yon12  13883  yon2  13884  yonpropd  13886  oppcyon  13887  yonffth  13902  yoniso  13903  plusffval  14214  sylow1lem2  14745  sylow2blem1  14766  sylow2blem2  14767  sylow3lem1  14773  sylow3lem6  14778  dmdprd  15071  dprdval  15073  staffval  15447  scaffval  15480  lpival  15829  ipffval  16384  cmpsub  16959  2ndcsep  17017  1stckgen  17081  kgencn2  17084  txcmplem1  17167  blbas  17808  met1stc  17899  nmfval  17943  qtopbaslem  18099  dchrptlem2  20336  dchrptlem3  20337  bafval  20990  vsfval  21021  trpredex  23408  brrestrict  23661  svli2  24650  svs2  24653  basexre  24688  bwt2  24758  indexdom  25579  heiborlem1  25701  isdrngo2  25755  isrngohom  25762  idlval  25804  isidl  25805  igenval  25852  lsatset  27869  dicval  30055
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 1926  ax-ext 2234  ax-sep 4038  ax-nul 4046  ax-pr 4108  ax-un 4403
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 1883  df-eu 2118  df-mo 2119  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-ne 2414  df-rex 2514  df-rab 2516  df-v 2729  df-dif 3081  df-un 3083  df-in 3085  df-ss 3089  df-nul 3363  df-if 3471  df-sn 3550  df-pr 3551  df-op 3553  df-uni 3728  df-br 3921  df-opab 3975  df-cnv 4596  df-dm 4598  df-rn 4599
  Copyright terms: Public domain W3C validator