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

Theorem rnex 6527
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 6525 . 2  |-  ( A  e.  _V  ->  ran  A  e.  _V )
31, 2ax-mp 5 1  |-  ran  A  e.  _V
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1756   _Vcvv 2987   ran crn 4856
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4428  ax-nul 4436  ax-pr 4546  ax-un 6387
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-rex 2736  df-rab 2739  df-v 2989  df-dif 3346  df-un 3348  df-in 3350  df-ss 3357  df-nul 3653  df-if 3807  df-sn 3893  df-pr 3895  df-op 3899  df-uni 4107  df-br 4308  df-opab 4366  df-cnv 4863  df-dm 4865  df-rn 4866
This theorem is referenced by:  elxp4  6537  elxp5  6538  ffoss  6553  fvclex  6564  abrexex  6566  wemoiso2  6578  2ndval  6595  fo2nd  6612  ixpsnf1o  7318  bren  7334  mapen  7490  ssenen  7500  sucdom2  7522  fodomfib  7606  hartogslem1  7771  brwdom  7797  unxpwdom2  7818  noinfep  7880  r0weon  8194  fseqen  8212  acnlem  8233  infpwfien  8247  aceq3lem  8305  dfac4  8307  dfac5  8313  dfac2  8315  dfac9  8320  dfac12lem2  8328  dfac12lem3  8329  infmap2  8402  cfflb  8443  infpssr  8492  fin23lem14  8517  fin23lem16  8519  fin23lem17  8522  fin23lem38  8533  fin23lem39  8534  axdc2lem  8632  axdc3lem2  8635  axcclem  8641  ttukeylem6  8698  wunex2  8920  wuncval2  8929  intgru  8996  wfgru  8998  qexALT  10983  hashfacen  12222  ccatfn  12287  shftfval  12574  vdwapval  14049  restfn  14378  prdsval  14408  wunfunc  14824  wunnat  14881  arwval  14926  catcfuccl  14992  catcxpccl  15032  yon11  15089  yon12  15090  yon2  15091  yonpropd  15093  oppcyon  15094  yonffth  15109  yoniso  15110  plusffval  15442  sylow1lem2  16113  sylow2blem1  16134  sylow2blem2  16135  sylow3lem1  16141  sylow3lem6  16146  dmdprd  16495  dprdval  16500  dprdvalOLD  16502  staffval  16947  scaffval  16981  lpival  17342  ipffval  18092  cmpsub  19018  bwthOLD  19029  2ndcsep  19078  1stckgen  19142  kgencn2  19145  txcmplem1  19229  blbas  20020  met1stc  20111  metutopOLD  20172  psmetutop  20173  nmfval  20196  qtopbaslem  20352  dchrptlem2  22619  dchrptlem3  22620  bafval  23997  vsfval  24028  ordtconlem1  26369  qqhval  26418  dya2icoseg2  26708  dya2iocuni  26713  sxbrsigalem2  26716  sxbrsigalem5  26718  trpredex  27716  brrestrict  27995  indexdom  28647  heiborlem1  28729  isdrngo2  28783  isrngohom  28790  idlval  28832  isidl  28833  igenval  28880  stoweidlem59  29873  lsatset  32654  dicval  34840
  Copyright terms: Public domain W3C validator