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

Theorem rnex 7265
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 𝐴 ∈ V
Assertion
Ref Expression
rnex ran 𝐴 ∈ V

Proof of Theorem rnex
StepHypRef Expression
1 dmex.1 . 2 𝐴 ∈ V
2 rnexg 7263 . 2 (𝐴 ∈ V → ran 𝐴 ∈ V)
31, 2ax-mp 5 1 ran 𝐴 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2139  Vcvv 3340  ran crn 5267
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pr 5055  ax-un 7114
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rex 3056  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-cnv 5274  df-dm 5276  df-rn 5277
This theorem is referenced by:  elxp4  7275  elxp5  7276  ffoss  7292  fvclex  7303  abrexexOLD  7307  wemoiso2  7319  2ndval  7336  fo2nd  7354  ixpsnf1o  8114  bren  8130  mapen  8289  ssenen  8299  sucdom2  8321  fodomfib  8405  hartogslem1  8612  brwdom  8637  unxpwdom2  8658  noinfep  8730  r0weon  9025  fseqen  9040  acnlem  9061  infpwfien  9075  aceq3lem  9133  dfac4  9135  dfac5  9141  dfac2b  9143  dfac2OLD  9145  dfac9  9150  dfac12lem2  9158  dfac12lem3  9159  infmap2  9232  cfflb  9273  infpssr  9322  fin23lem14  9347  fin23lem16  9349  fin23lem17  9352  fin23lem38  9363  fin23lem39  9364  axdc2lem  9462  axdc3lem2  9465  axcclem  9471  ttukeylem6  9528  wunex2  9752  wuncval2  9761  intgru  9828  wfgru  9830  qexALT  11996  hashfacen  13430  shftfval  14009  vdwapval  15879  restfn  16287  prdsval  16317  wunfunc  16760  wunnat  16817  arwval  16894  catcfuccl  16960  catcxpccl  17048  yon11  17105  yon12  17106  yon2  17107  yonpropd  17109  oppcyon  17110  yonffth  17125  yoniso  17126  plusffval  17448  sylow1lem2  18214  sylow2blem1  18235  sylow2blem2  18236  sylow3lem1  18242  sylow3lem6  18247  dmdprd  18597  dprdval  18602  staffval  19049  scaffval  19083  lpival  19447  ipffval  20195  cmpsub  21405  2ndcsep  21464  1stckgen  21559  kgencn2  21562  txcmplem1  21646  blbas  22436  met1stc  22527  psmetutop  22573  nmfval  22594  qtopbaslem  22763  dchrptlem2  25189  dchrptlem3  25190  ishpg  25850  edgval  26140  edgvalOLD  26141  bafval  27768  vsfval  27797  foresf1o  29650  locfinreflem  30216  cmpcref  30226  ordtconnlem1  30279  qqhval  30327  sigapildsys  30534  dya2icoseg2  30649  dya2iocuni  30654  sxbrsigalem2  30657  sxbrsigalem5  30659  omssubadd  30671  mvtval  31704  mvrsval  31709  mstaval  31748  trpredex  32042  brrestrict  32362  relowlssretop  33522  cnfinltrel  33552  lindsdom  33716  indexdom  33842  heiborlem1  33923  isdrngo2  34070  isrngohom  34077  idlval  34125  isidl  34126  igenval  34173  lsatset  34780  dicval  36967  trclexi  38429  rtrclexi  38430  dfrtrcl5  38438  dfrcl2  38468  stoweidlem59  40779  fourierdlem71  40897  salgensscntex  41065  aacllem  43060
  Copyright terms: Public domain W3C validator