Theorem rnex 7854

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 7846	. 2 ⊢ (𝐴 ∈ V → ran 𝐴 ∈ V)
3	1, 2	ax-mp 5	1 ⊢ ran 𝐴 ∈ V

Syntax hints:   ∈ wcel 2114  Vcvv 3430  ran crn 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5231  ax-pr 5370  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-cnv 5632  df-dm 5634  df-rn 5635

This theorem is referenced by:  elxp4  7866  elxp5  7867  ffoss  7892  fvclex  7905  wemoiso2  7920  2ndval  7938  fo2nd  7956  mapfoss  8792  ixpsnf1o  8879  bren  8896  mapen  9072  ssenen  9082  sucdom2  9130  fodomfib  9232  fodomfibOLD  9234  hartogslem1  9450  brwdom  9475  unxpwdom2  9496  noinfep  9572  r0weon  9925  fseqen  9940  acnlem  9961  infpwfien  9975  aceq3lem  10033  dfac4  10035  dfac5  10042  dfac2b  10044  dfac9  10050  dfac12lem2  10058  dfac12lem3  10059  infmap2  10130  cfflb  10172  infpssr  10221  fin23lem14  10246  fin23lem16  10248  fin23lem17  10251  fin23lem38  10262  fin23lem39  10263  axdc2lem  10361  axdc3lem2  10364  axcclem  10370  ttukeylem6  10427  wunex2  10652  wuncval2  10661  intgru  10728  wfgru  10730  qexALT  12905  seqexw  13970  shftfval  15023  vdwapval  16935  restfn  17378  prdsvallem  17408  prdsval  17409  wunfunc  17859  wunnat  17917  arwval  18001  catcfuccl  18076  catcxpccl  18164  yon11  18221  yon12  18222  yon2  18223  yonpropd  18225  oppcyon  18226  yonffth  18241  yoniso  18242  plusffval  18605  grpsubfval  18950  mulgfval  19036  sylow1lem2  19565  sylow2blem1  19586  sylow2blem2  19587  sylow3lem1  19593  sylow3lem6  19598  dmdprd  19966  dprdval  19971  staffval  20809  scaffval  20866  lpival  21314  ipffval  21638  cmpsub  23375  2ndcsep  23434  1stckgen  23529  kgencn2  23532  txcmplem1  23616  blbas  24405  met1stc  24496  psmetutop  24542  nmfval  24563  dchrptlem2  27242  dchrptlem3  27243  mulsproplem9  28130  ishpg  28841  edgval  29132  bafval  30690  vsfval  30719  foresf1o  32589  fnpreimac  32758  nsgmgc  33487  nsgqusf1o  33491  idlsrgtset  33583  locfinreflem  34000  cmpcref  34010  rspectopn  34027  ordtconnlem1  34084  qqhval  34132  sigapildsys  34322  dya2icoseg2  34438  dya2iocuni  34443  sxbrsigalem2  34446  sxbrsigalem5  34448  omssubadd  34460  mvtval  35698  mvrsval  35703  mstaval  35742  brrestrict  36147  relowlssretop  37693  exrecfnlem  37709  ctbssinf  37736  lindsdom  37949  indexdom  38069  heiborlem1  38146  isdrngo2  38293  isrngohom  38300  idlval  38348  isidl  38349  igenval  38396  lsatset  39450  dicval  41636  aks6d1c6isolem2  42628  prjcrvfval  43078  trclexi  44065  rtrclexi  44066  dfrtrcl5  44074  dfrcl2  44119  wfaxrep  45439  stoweidlem59  46505  fourierdlem71  46623  salgensscntex  46790  aacllem  50288