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

Theorem rnex 7610
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 7607 . 2 (𝐴 ∈ V → ran 𝐴 ∈ V)
31, 2ax-mp 5 1 ran 𝐴 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2107  Vcvv 3500  ran crn 5555
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2798  ax-sep 5200  ax-nul 5207  ax-pr 5326  ax-un 7455
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2620  df-eu 2652  df-clab 2805  df-cleq 2819  df-clel 2898  df-nfc 2968  df-rex 3149  df-rab 3152  df-v 3502  df-dif 3943  df-un 3945  df-in 3947  df-ss 3956  df-nul 4296  df-if 4471  df-sn 4565  df-pr 4567  df-op 4571  df-uni 4838  df-br 5064  df-opab 5126  df-cnv 5562  df-dm 5564  df-rn 5565
This theorem is referenced by:  elxp4  7620  elxp5  7621  ffoss  7643  fvclex  7656  wemoiso2  7671  2ndval  7688  fo2nd  7706  ixpsnf1o  8496  bren  8512  mapen  8675  ssenen  8685  sucdom2  8708  fodomfib  8792  hartogslem1  9000  brwdom  9025  unxpwdom2  9046  noinfep  9117  r0weon  9432  fseqen  9447  acnlem  9468  infpwfien  9482  aceq3lem  9540  dfac4  9542  dfac5  9548  dfac2b  9550  dfac9  9556  dfac12lem2  9564  dfac12lem3  9565  infmap2  9634  cfflb  9675  infpssr  9724  fin23lem14  9749  fin23lem16  9751  fin23lem17  9754  fin23lem38  9765  fin23lem39  9766  axdc2lem  9864  axdc3lem2  9867  axcclem  9873  ttukeylem6  9930  wunex2  10154  wuncval2  10163  intgru  10230  wfgru  10232  qexALT  12358  seqexw  13380  hashfacen  13807  shftfval  14424  vdwapval  16304  restfn  16693  prdsval  16723  wunfunc  17164  wunnat  17221  arwval  17298  catcfuccl  17364  catcxpccl  17452  yon11  17509  yon12  17510  yon2  17511  yonpropd  17513  oppcyon  17514  yonffth  17529  yoniso  17530  plusffval  17853  grpsubfval  18092  mulgfval  18171  sylow1lem2  18660  sylow2blem1  18681  sylow2blem2  18682  sylow3lem1  18688  sylow3lem6  18693  dmdprd  19056  dprdval  19061  staffval  19554  scaffval  19588  lpival  19953  ipffval  20727  cmpsub  21943  2ndcsep  22002  1stckgen  22097  kgencn2  22100  txcmplem1  22184  blbas  22974  met1stc  23065  psmetutop  23111  nmfval  23132  dchrptlem2  25774  dchrptlem3  25775  ishpg  26478  edgval  26767  bafval  28314  vsfval  28343  foresf1o  30198  fnpreimac  30350  locfinreflem  31009  cmpcref  31019  ordtconnlem1  31072  qqhval  31120  sigapildsys  31326  dya2icoseg2  31441  dya2iocuni  31446  sxbrsigalem2  31449  sxbrsigalem5  31451  omssubadd  31463  mvtval  32650  mvrsval  32655  mstaval  32694  trpredex  32979  brrestrict  33313  relowlssretop  34532  exrecfnlem  34548  ctbssinf  34575  lindsdom  34772  indexdom  34896  heiborlem1  34976  isdrngo2  35123  isrngohom  35130  idlval  35178  isidl  35179  igenval  35226  lsatset  36012  dicval  38198  trclexi  39864  rtrclexi  39865  dfrtrcl5  39873  dfrcl2  39903  stoweidlem59  42229  fourierdlem71  42347  salgensscntex  42512  aacllem  44804
  Copyright terms: Public domain W3C validator