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

Theorem rnex 4942
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 4940 . 2  |-  ( A  e.  _V  ->  ran  A  e.  _V )
31, 2ax-mp 8 1  |-  ran  A  e.  _V
Colors of variables: wff set class
Syntax hints:    e. wcel 1684   _Vcvv 2788   ran crn 4690
This theorem is referenced by:  elxp4  5160  elxp5  5161  ffoss  5505  fvclex  5761  abrexex  5763  wemoiso2  5856  2ndval  6125  fo2nd  6140  ixpsnf1o  6856  bren  6871  mapen  7025  ssenen  7035  sucdom2  7057  fodomfib  7136  hartogslem1  7257  brwdom  7281  unxpwdom2  7302  noinfep  7360  r0weon  7640  fseqen  7654  acnlem  7675  infpwfien  7689  aceq3lem  7747  dfac4  7749  dfac5  7755  dfac2  7757  dfac9  7762  dfac12lem2  7770  dfac12lem3  7771  infmap2  7844  cfflb  7885  infpssr  7934  fin23lem14  7959  fin23lem16  7961  fin23lem17  7964  fin23lem38  7975  fin23lem39  7976  axdc2lem  8074  axdc3lem2  8077  axcclem  8083  ttukeylem6  8141  wunex2  8360  wuncval2  8369  intgru  8436  wfgru  8438  qexALT  10331  hashfacen  11392  ccatfn  11427  shftfval  11565  vdwapval  13020  restfn  13329  prdsval  13355  wunfunc  13773  wunnat  13830  arwval  13875  catcfuccl  13941  catcxpccl  13981  yon11  14038  yon12  14039  yon2  14040  yonpropd  14042  oppcyon  14043  yonffth  14058  yoniso  14059  plusffval  14379  sylow1lem2  14910  sylow2blem1  14931  sylow2blem2  14932  sylow3lem1  14938  sylow3lem6  14943  dmdprd  15236  dprdval  15238  staffval  15612  scaffval  15645  lpival  15997  ipffval  16552  cmpsub  17127  2ndcsep  17185  1stckgen  17249  kgencn2  17252  txcmplem1  17335  blbas  17976  met1stc  18067  nmfval  18111  qtopbaslem  18267  dchrptlem2  20504  dchrptlem3  20505  bafval  21160  vsfval  21191  dya2iocrfn  23580  dya2iocct  23581  dya2iocrrnval  23582  trpredex  24240  brrestrict  24487  svli2  25484  svs2  25487  basexre  25522  bwt2  25592  indexdom  26413  heiborlem1  26535  isdrngo2  26589  isrngohom  26596  idlval  26638  isidl  26639  igenval  26686  stoweidlem59  27808  lsatset  29180  dicval  31366
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214  ax-un 4512
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-rex 2549  df-rab 2552  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-cnv 4697  df-dm 4699  df-rn 4700
  Copyright terms: Public domain W3C validator