Theorem rnex 7852

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

Syntax hints:   ∈ wcel 2113  Vcvv 3440  ran crn 5625

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-cnv 5632  df-dm 5634  df-rn 5635

This theorem is referenced by:  elxp4  7864  elxp5  7865  ffoss  7890  fvclex  7903  wemoiso2  7918  2ndval  7936  fo2nd  7954  mapfoss  8789  ixpsnf1o  8876  bren  8893  mapen  9069  ssenen  9079  sucdom2  9127  fodomfib  9229  fodomfibOLD  9231  hartogslem1  9447  brwdom  9472  unxpwdom2  9493  noinfep  9569  r0weon  9922  fseqen  9937  acnlem  9958  infpwfien  9972  aceq3lem  10030  dfac4  10032  dfac5  10039  dfac2b  10041  dfac9  10047  dfac12lem2  10055  dfac12lem3  10056  infmap2  10127  cfflb  10169  infpssr  10218  fin23lem14  10243  fin23lem16  10245  fin23lem17  10248  fin23lem38  10259  fin23lem39  10260  axdc2lem  10358  axdc3lem2  10361  axcclem  10367  ttukeylem6  10424  wunex2  10649  wuncval2  10658  intgru  10725  wfgru  10727  qexALT  12877  seqexw  13940  shftfval  14993  vdwapval  16901  restfn  17344  prdsvallem  17374  prdsval  17375  wunfunc  17825  wunnat  17883  arwval  17967  catcfuccl  18042  catcxpccl  18130  yon11  18187  yon12  18188  yon2  18189  yonpropd  18191  oppcyon  18192  yonffth  18207  yoniso  18208  plusffval  18571  grpsubfval  18913  mulgfval  18999  sylow1lem2  19528  sylow2blem1  19549  sylow2blem2  19550  sylow3lem1  19556  sylow3lem6  19561  dmdprd  19929  dprdval  19934  staffval  20774  scaffval  20831  lpival  21279  ipffval  21603  cmpsub  23344  2ndcsep  23403  1stckgen  23498  kgencn2  23501  txcmplem1  23585  blbas  24374  met1stc  24465  psmetutop  24511  nmfval  24532  dchrptlem2  27232  dchrptlem3  27233  mulsproplem9  28120  ishpg  28831  edgval  29122  bafval  30679  vsfval  30708  foresf1o  32579  fnpreimac  32749  nsgmgc  33493  nsgqusf1o  33497  idlsrgtset  33589  locfinreflem  33997  cmpcref  34007  rspectopn  34024  ordtconnlem1  34081  qqhval  34129  sigapildsys  34319  dya2icoseg2  34435  dya2iocuni  34440  sxbrsigalem2  34443  sxbrsigalem5  34445  omssubadd  34457  mvtval  35694  mvrsval  35699  mstaval  35738  brrestrict  36143  relowlssretop  37568  exrecfnlem  37584  ctbssinf  37611  lindsdom  37815  indexdom  37935  heiborlem1  38012  isdrngo2  38159  isrngohom  38166  idlval  38214  isidl  38215  igenval  38262  lsatset  39250  dicval  41436  aks6d1c6isolem2  42429  prjcrvfval  42874  trclexi  43861  rtrclexi  43862  dfrtrcl5  43870  dfrcl2  43915  wfaxrep  45235  stoweidlem59  46303  fourierdlem71  46421  salgensscntex  46588  aacllem  50046