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

Theorem rnex 6482
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
Assertion
Ref Expression
rnex

Proof of Theorem rnex
StepHypRef Expression
1 dmex.1 . 2
2 rnexg 6480 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1749   cvv 2951  rancrn 4812
This theorem is referenced by:  elxp4  6492  elxp5  6493  ffoss  6507  fvclex  6518  abrexex  6520  wemoiso2  6532  2ndval  6549  fo2nd  6566  ixpsnf1o  7262  bren  7278  mapen  7434  ssenen  7444  sucdom2  7466  fodomfib  7550  hartogslem1  7703  brwdom  7729  unxpwdom2  7750  noinfep  7812  r0weon  8126  fseqen  8144  acnlem  8165  infpwfien  8179  aceq3lem  8237  dfac4  8239  dfac5  8245  dfac2  8247  dfac9  8252  dfac12lem2  8260  dfac12lem3  8261  infmap2  8334  cfflb  8375  infpssr  8424  fin23lem14  8449  fin23lem16  8451  fin23lem17  8454  fin23lem38  8465  fin23lem39  8466  axdc2lem  8564  axdc3lem2  8567  axcclem  8573  ttukeylem6  8630  wunex2  8851  wuncval2  8860  intgru  8927  wfgru  8929  qexALT  10913  hashfacen  12148  ccatfn  12213  shftfval  12500  vdwapval  13974  restfn  14303  prdsval  14333  wunfunc  14749  wunnat  14806  arwval  14851  catcfuccl  14917  catcxpccl  14957  yon11  15014  yon12  15015  yon2  15016  yonpropd  15018  oppcyon  15019  yonffth  15034  yoniso  15035  plusffval  15367  sylow1lem2  16035  sylow2blem1  16056  sylow2blem2  16057  sylow3lem1  16063  sylow3lem6  16068  dmdprd  16368  dprdval  16370  staffval  16745  scaffval  16779  lpival  17136  ipffval  17785  cmpsub  18707  bwthOLD  18718  2ndcsep  18767  1stckgen  18831  kgencn2  18834  txcmplem1  18918  blbas  19705  met1stc  19796  metutopOLD  19857  psmetutop  19858  nmfval  19881  qtopbaslem  20037  dchrptlem2  22345  dchrptlem3  22346  bafval  23661  vsfval  23692  ordtconlem1  26063  qqhval  26112  dya2icoseg2  26402  dya2iocuni  26407  sxbrsigalem2  26410  sxbrsigalem5  26412  trpredex  27403  brrestrict  27682  indexdom  28299  heiborlem1  28381  isdrngo2  28435  isrngohom  28442  idlval  28484  isidl  28485  igenval  28532  stoweidlem59  29528  lsatset  32072  dicval  34258
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1586  ax-4 1597  ax-5 1661  ax-6 1701  ax-7 1721  ax-8 1751  ax-9 1753  ax-10 1768  ax-11 1773  ax-12 1785  ax-13 1934  ax-ext 2403  ax-sep 4388  ax-nul 4396  ax-pr 4503  ax-un 6342
This theorem depends on definitions:  df-bi 179  df-or 363  df-an 364  df-3an 952  df-tru 1355  df-ex 1582  df-nf 1585  df-sb 1694  df-eu 2248  df-mo 2249  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2547  df-ne 2587  df-rex 2700  df-rab 2703  df-v 2953  df-dif 3308  df-un 3310  df-in 3312  df-ss 3319  df-nul 3615  df-if 3769  df-sn 3859  df-pr 3860  df-op 3862  df-uni 4067  df-br 4268  df-opab 4326  df-cnv 4819  df-dm 4821  df-rn 4822
  Copyright terms: Public domain W3C validator