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

Theorem rnex 6719
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 6717 . 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 1804   _Vcvv 3095   ran crn 4990
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pr 4676  ax-un 6577
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-rex 2799  df-rab 2802  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-cnv 4997  df-dm 4999  df-rn 5000
This theorem is referenced by:  elxp4  6729  elxp5  6730  ffoss  6746  fvclex  6757  abrexex  6759  wemoiso2  6771  2ndval  6788  fo2nd  6806  ixpsnf1o  7511  bren  7527  mapen  7683  ssenen  7693  sucdom2  7716  fodomfib  7802  hartogslem1  7970  brwdom  7996  unxpwdom2  8017  noinfep  8079  r0weon  8393  fseqen  8411  acnlem  8432  infpwfien  8446  aceq3lem  8504  dfac4  8506  dfac5  8512  dfac2  8514  dfac9  8519  dfac12lem2  8527  dfac12lem3  8528  infmap2  8601  cfflb  8642  infpssr  8691  fin23lem14  8716  fin23lem16  8718  fin23lem17  8721  fin23lem38  8732  fin23lem39  8733  axdc2lem  8831  axdc3lem2  8834  axcclem  8840  ttukeylem6  8897  wunex2  9119  wuncval2  9128  intgru  9195  wfgru  9197  qexALT  11208  hashfacen  12485  ccatfn  12573  shftfval  12885  vdwapval  14473  restfn  14804  prdsval  14834  wunfunc  15247  wunnat  15304  arwval  15349  catcfuccl  15415  catcxpccl  15455  yon11  15512  yon12  15513  yon2  15514  yonpropd  15516  oppcyon  15517  yonffth  15532  yoniso  15533  plusffval  15856  sylow1lem2  16598  sylow2blem1  16619  sylow2blem2  16620  sylow3lem1  16626  sylow3lem6  16631  dmdprd  17008  dprdval  17013  dprdvalOLD  17015  staffval  17475  scaffval  17509  lpival  17872  ipffval  18661  cmpsub  19878  bwthOLD  19889  2ndcsep  19938  1stckgen  20033  kgencn2  20036  txcmplem1  20120  blbas  20911  met1stc  21002  metutopOLD  21063  psmetutop  21064  nmfval  21087  qtopbaslem  21243  dchrptlem2  23518  dchrptlem3  23519  ishpg  24106  edgval  24317  bafval  25475  vsfval  25506  foresf1o  27381  locfinreflem  27821  cmpcref  27831  ordtconlem1  27884  qqhval  27933  dya2icoseg2  28227  dya2iocuni  28232  sxbrsigalem2  28235  sxbrsigalem5  28237  mvtval  28838  mvrsval  28843  mstaval  28882  trpredex  29296  brrestrict  29575  indexdom  30201  heiborlem1  30283  isdrngo2  30337  isrngohom  30344  idlval  30386  isidl  30387  igenval  30434  stoweidlem59  31795  fourierdlem71  31914  lsatset  34590  dicval  36778  trclub  37612  trclubg  37613
  Copyright terms: Public domain W3C validator