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

Theorem rnex 6741
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 6739 . 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 1870   _Vcvv 3087   ran crn 4855
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pr 4661  ax-un 6597
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-rex 2788  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-uni 4223  df-br 4427  df-opab 4485  df-cnv 4862  df-dm 4864  df-rn 4865
This theorem is referenced by:  elxp4  6751  elxp5  6752  ffoss  6768  fvclex  6779  abrexex  6781  wemoiso2  6793  2ndval  6810  fo2nd  6828  ixpsnf1o  7570  bren  7586  mapen  7742  ssenen  7752  sucdom2  7774  fodomfib  7857  hartogslem1  8057  brwdom  8082  unxpwdom2  8103  noinfep  8164  r0weon  8442  fseqen  8456  acnlem  8477  infpwfien  8491  aceq3lem  8549  dfac4  8551  dfac5  8557  dfac2  8559  dfac9  8564  dfac12lem2  8572  dfac12lem3  8573  infmap2  8646  cfflb  8687  infpssr  8736  fin23lem14  8761  fin23lem16  8763  fin23lem17  8766  fin23lem38  8777  fin23lem39  8778  axdc2lem  8876  axdc3lem2  8879  axcclem  8885  ttukeylem6  8942  wunex2  9162  wuncval2  9171  intgru  9238  wfgru  9240  qexALT  11279  hashfacen  12612  ccatfnOLD  12705  shftfval  13112  vdwapval  14877  restfn  15273  prdsval  15303  wunfunc  15746  wunnat  15803  arwval  15880  catcfuccl  15946  catcxpccl  16034  yon11  16091  yon12  16092  yon2  16093  yonpropd  16095  oppcyon  16096  yonffth  16111  yoniso  16112  plusffval  16435  sylow1lem2  17177  sylow2blem1  17198  sylow2blem2  17199  sylow3lem1  17205  sylow3lem6  17210  dmdprd  17556  dprdval  17561  staffval  18001  scaffval  18035  lpival  18395  ipffval  19137  cmpsub  20337  2ndcsep  20396  1stckgen  20491  kgencn2  20494  txcmplem1  20578  blbas  21367  met1stc  21458  psmetutop  21504  nmfval  21525  qtopbaslem  21681  dchrptlem2  24047  dchrptlem3  24048  ishpg  24648  edgval  24903  bafval  26059  vsfval  26090  foresf1o  27966  locfinreflem  28497  cmpcref  28507  ordtconlem1  28560  qqhval  28608  sigapildsys  28814  dya2icoseg2  28930  dya2iocuni  28935  sxbrsigalem2  28938  sxbrsigalem5  28940  omssubadd  28952  mvtval  29917  mvrsval  29922  mstaval  29961  trpredex  30256  brrestrict  30492  relowlssretop  31491  indexdom  31755  heiborlem1  31837  isdrngo2  31891  isrngohom  31898  idlval  31940  isidl  31941  igenval  31988  lsatset  32255  dicval  34443  dfrcl2  35895  stoweidlem59  37479  fourierdlem71  37599  aacllem  39291
  Copyright terms: Public domain W3C validator