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

Theorem rnex 7605
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 7602 . 2 (𝐴 ∈ V → ran 𝐴 ∈ V)
31, 2ax-mp 5 1 ran 𝐴 ∈ V
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  Vcvv 3495  ran crn 5550
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rex 3144  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-opab 5121  df-cnv 5557  df-dm 5559  df-rn 5560
This theorem is referenced by:  elxp4  7615  elxp5  7616  ffoss  7638  fvclex  7651  wemoiso2  7666  2ndval  7683  fo2nd  7701  ixpsnf1o  8491  bren  8507  mapen  8670  ssenen  8680  sucdom2  8703  fodomfib  8787  hartogslem1  8995  brwdom  9020  unxpwdom2  9041  noinfep  9112  r0weon  9427  fseqen  9442  acnlem  9463  infpwfien  9477  aceq3lem  9535  dfac4  9537  dfac5  9543  dfac2b  9545  dfac9  9551  dfac12lem2  9559  dfac12lem3  9560  infmap2  9629  cfflb  9670  infpssr  9719  fin23lem14  9744  fin23lem16  9746  fin23lem17  9749  fin23lem38  9760  fin23lem39  9761  axdc2lem  9859  axdc3lem2  9862  axcclem  9868  ttukeylem6  9925  wunex2  10149  wuncval2  10158  intgru  10225  wfgru  10227  qexALT  12353  seqexw  13375  hashfacen  13802  shftfval  14419  vdwapval  16299  restfn  16688  prdsval  16718  wunfunc  17159  wunnat  17216  arwval  17293  catcfuccl  17359  catcxpccl  17447  yon11  17504  yon12  17505  yon2  17506  yonpropd  17508  oppcyon  17509  yonffth  17524  yoniso  17525  plusffval  17848  grpsubfval  18087  mulgfval  18166  sylow1lem2  18655  sylow2blem1  18676  sylow2blem2  18677  sylow3lem1  18683  sylow3lem6  18688  dmdprd  19051  dprdval  19056  staffval  19549  scaffval  19583  lpival  19948  ipffval  20722  cmpsub  21938  2ndcsep  21997  1stckgen  22092  kgencn2  22095  txcmplem1  22179  blbas  22969  met1stc  23060  psmetutop  23106  nmfval  23127  dchrptlem2  25769  dchrptlem3  25770  ishpg  26473  edgval  26762  bafval  28309  vsfval  28338  foresf1o  30193  fnpreimac  30345  locfinreflem  31004  cmpcref  31014  ordtconnlem1  31067  qqhval  31115  sigapildsys  31321  dya2icoseg2  31436  dya2iocuni  31441  sxbrsigalem2  31444  sxbrsigalem5  31446  omssubadd  31458  mvtval  32645  mvrsval  32650  mstaval  32689  trpredex  32974  brrestrict  33308  relowlssretop  34527  exrecfnlem  34543  ctbssinf  34570  lindsdom  34768  indexdom  34892  heiborlem1  34972  isdrngo2  35119  isrngohom  35126  idlval  35174  isidl  35175  igenval  35222  lsatset  36008  dicval  38194  trclexi  39860  rtrclexi  39861  dfrtrcl5  39869  dfrcl2  39899  stoweidlem59  42225  fourierdlem71  42343  salgensscntex  42508  aacllem  44800
  Copyright terms: Public domain W3C validator