Theorem rnex 7850

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

Syntax hints:   ∈ wcel 2119  Vcvv 3431  ran crn 5619

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711  ax-sep 5218  ax-pr 5362  ax-un 7678

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-cnv 5626  df-dm 5628  df-rn 5629

This theorem is referenced by:  elxp4  7862  elxp5  7863  ffoss  7888  fvclex  7901  wemoiso2  7916  2ndval  7934  fo2nd  7952  mapfoss  8789  ixpsnf1o  8876  bren  8893  mapen  9069  ssenen  9079  sucdom2  9127  fodomfib  9229  fodomfibOLD  9231  hartogslem1  9447  brwdom  9472  unxpwdom2  9493  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  20813  scaffval  20870  lpival  21317  ipffval  21623  cmpsub  23383  2ndcsep  23442  1stckgen  23537  kgencn2  23540  txcmplem1  23624  blbas  24413  met1stc  24504  psmetutop  24550  nmfval  24571  dchrptlem2  27246  dchrptlem3  27247  mulsproplem9  28134  ishpg  28845  edgval  29136  bafval  30693  vsfval  30722  foresf1o  32592  fnpreimac  32762  nsgmgc  33495  nsgqusf1o  33499  idlsrgtset  33591  locfinreflem  34024  cmpcref  34034  rspectopn  34051  ordtconnlem1  34108  qqhval  34156  sigapildsys  34346  dya2icoseg2  34462  dya2iocuni  34467  sxbrsigalem2  34470  sxbrsigalem5  34472  omssubadd  34484  mvtval  35728  mvrsval  35733  mstaval  35772  brrestrict  36177  relowlssretop  37725  exrecfnlem  37741  ctbssinf  37768  lindsdom  37981  indexdom  38101  heiborlem1  38178  isdrngo2  38325  isrngohom  38332  idlval  38380  isidl  38381  igenval  38428  lsatset  39482  dicval  41668  aks6d1c6isolem2  42660  prjcrvfval  43081  trclexi  44064  rtrclexi  44065  dfrtrcl5  44073  dfrcl2  44118  wfaxrep  45438  stoweidlem59  46502  fourierdlem71  46620  salgensscntex  46787  aacllem  50291