Theorem rnex 7100

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

Step	Hyp	Ref	Expression
1		dmex.1	. 2 ⊢ 𝐴 ∈ V
2		rnexg 7098	. 2 ⊢ (𝐴 ∈ V → ran 𝐴 ∈ V)
3	1, 2	ax-mp 5	1 ⊢ ran 𝐴 ∈ V

Syntax hints:   ∈ wcel 1990  Vcvv 3200  ran crn 5115

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-cnv 5122  df-dm 5124  df-rn 5125

This theorem is referenced by:  elxp4  7110  elxp5  7111  ffoss  7127  fvclex  7138  abrexexOLD  7142  wemoiso2  7154  2ndval  7171  fo2nd  7189  ixpsnf1o  7948  bren  7964  mapen  8124  ssenen  8134  sucdom2  8156  fodomfib  8240  hartogslem1  8447  brwdom  8472  unxpwdom2  8493  noinfep  8557  r0weon  8835  fseqen  8850  acnlem  8871  infpwfien  8885  aceq3lem  8943  dfac4  8945  dfac5  8951  dfac2  8953  dfac9  8958  dfac12lem2  8966  dfac12lem3  8967  infmap2  9040  cfflb  9081  infpssr  9130  fin23lem14  9155  fin23lem16  9157  fin23lem17  9160  fin23lem38  9171  fin23lem39  9172  axdc2lem  9270  axdc3lem2  9273  axcclem  9279  ttukeylem6  9336  wunex2  9560  wuncval2  9569  intgru  9636  wfgru  9638  qexALT  11803  hashfacen  13238  shftfval  13810  vdwapval  15677  restfn  16085  prdsval  16115  wunfunc  16559  wunnat  16616  arwval  16693  catcfuccl  16759  catcxpccl  16847  yon11  16904  yon12  16905  yon2  16906  yonpropd  16908  oppcyon  16909  yonffth  16924  yoniso  16925  plusffval  17247  sylow1lem2  18014  sylow2blem1  18035  sylow2blem2  18036  sylow3lem1  18042  sylow3lem6  18047  dmdprd  18397  dprdval  18402  staffval  18847  scaffval  18881  lpival  19245  ipffval  19993  cmpsub  21203  2ndcsep  21262  1stckgen  21357  kgencn2  21360  txcmplem1  21444  blbas  22235  met1stc  22326  psmetutop  22372  nmfval  22393  qtopbaslem  22562  dchrptlem2  24990  dchrptlem3  24991  ishpg  25651  edgval  25941  edgvalOLD  25942  bafval  27459  vsfval  27488  foresf1o  29343  locfinreflem  29907  cmpcref  29917  ordtconnlem1  29970  qqhval  30018  sigapildsys  30225  dya2icoseg2  30340  dya2iocuni  30345  sxbrsigalem2  30348  sxbrsigalem5  30350  omssubadd  30362  mvtval  31397  mvrsval  31402  mstaval  31441  trpredex  31737  brrestrict  32056  relowlssretop  33211  lindsdom  33403  indexdom  33529  heiborlem1  33610  isdrngo2  33757  isrngohom  33764  idlval  33812  isidl  33813  igenval  33860  lsatset  34277  dicval  36465  trclexi  37927  rtrclexi  37928  dfrtrcl5  37936  dfrcl2  37966  stoweidlem59  40276  fourierdlem71  40394  salgensscntex  40562  aacllem  42547