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

Theorem rnex 6645
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 6643 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  e.wcel 1758   cvv 3081  rancrn 4958
This theorem is referenced by:  elxp4  6655  elxp5  6656  ffoss  6671  fvclex  6682  abrexex  6684  wemoiso2  6696  2ndval  6713  fo2nd  6730  ixpsnf1o  7437  bren  7453  mapen  7609  ssenen  7619  sucdom2  7642  fodomfib  7726  hartogslem1  7893  brwdom  7919  unxpwdom2  7940  noinfep  8002  r0weon  8316  fseqen  8334  acnlem  8355  infpwfien  8369  aceq3lem  8427  dfac4  8429  dfac5  8435  dfac2  8437  dfac9  8442  dfac12lem2  8450  dfac12lem3  8451  infmap2  8524  cfflb  8565  infpssr  8614  fin23lem14  8639  fin23lem16  8641  fin23lem17  8644  fin23lem38  8655  fin23lem39  8656  axdc2lem  8754  axdc3lem2  8757  axcclem  8763  ttukeylem6  8820  wunex2  9042  wuncval2  9051  intgru  9118  wfgru  9120  qexALT  11107  hashfacen  12365  ccatfn  12430  shftfval  12717  vdwapval  14192  restfn  14522  prdsval  14552  wunfunc  14968  wunnat  15025  arwval  15070  catcfuccl  15136  catcxpccl  15176  yon11  15233  yon12  15234  yon2  15235  yonpropd  15237  oppcyon  15238  yonffth  15253  yoniso  15254  plusffval  15586  sylow1lem2  16259  sylow2blem1  16280  sylow2blem2  16281  sylow3lem1  16287  sylow3lem6  16292  dmdprd  16655  dprdval  16660  dprdvalOLD  16662  staffval  17108  scaffval  17142  lpival  17503  ipffval  18270  cmpsub  19402  bwthOLD  19413  2ndcsep  19462  1stckgen  19526  kgencn2  19529  txcmplem1  19613  blbas  20404  met1stc  20495  metutopOLD  20556  psmetutop  20557  nmfval  20580  qtopbaslem  20736  dchrptlem2  23004  dchrptlem3  23005  bafval  24451  vsfval  24482  ordtconlem1  26811  qqhval  26860  dya2icoseg2  27149  dya2iocuni  27154  sxbrsigalem2  27157  sxbrsigalem5  27159  trpredex  28157  brrestrict  28436  indexdom  29088  heiborlem1  29170  isdrngo2  29224  isrngohom  29231  idlval  29273  isidl  29274  igenval  29321  stoweidlem59  30588  lsatset  33486  dicval  35672
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4530  ax-nul 4538  ax-pr 4648  ax-un 6505
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-rex 2806  df-rab 2809  df-v 3083  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3752  df-if 3906  df-sn 3994  df-pr 3996  df-op 4000  df-uni 4209  df-br 4410  df-opab 4468  df-cnv 4965  df-dm 4967  df-rn 4968
  Copyright terms: Public domain W3C validator