Theorem rnex 7690

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

Syntax hints:   ∈ wcel 2110  Vcvv 3408  ran crn 5552

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322  ax-un 7523

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-opab 5116  df-cnv 5559  df-dm 5561  df-rn 5562

This theorem is referenced by:  elxp4  7700  elxp5  7701  ffoss  7719  fvclex  7732  wemoiso2  7747  2ndval  7764  fo2nd  7782  mapfoss  8533  ixpsnf1o  8619  bren  8636  brenOLD  8637  sucdom2  8755  mapen  8810  ssenen  8820  fodomfib  8950  hartogslem1  9158  brwdom  9183  unxpwdom2  9204  noinfep  9275  trpredex  9343  r0weon  9626  fseqen  9641  acnlem  9662  infpwfien  9676  aceq3lem  9734  dfac4  9736  dfac5  9742  dfac2b  9744  dfac9  9750  dfac12lem2  9758  dfac12lem3  9759  infmap2  9832  cfflb  9873  infpssr  9922  fin23lem14  9947  fin23lem16  9949  fin23lem17  9952  fin23lem38  9963  fin23lem39  9964  axdc2lem  10062  axdc3lem2  10065  axcclem  10071  ttukeylem6  10128  wunex2  10352  wuncval2  10361  intgru  10428  wfgru  10430  qexALT  12560  seqexw  13590  hashfacenOLD  14019  shftfval  14633  vdwapval  16526  restfn  16929  prdsvallem  16959  prdsval  16960  wunfunc  17405  wunfuncOLD  17406  wunnat  17463  wunnatOLD  17464  arwval  17549  catcfuccl  17625  catcfucclOLD  17626  catcxpccl  17714  catcxpcclOLD  17715  yon11  17772  yon12  17773  yon2  17774  yonpropd  17776  oppcyon  17777  yonffth  17792  yoniso  17793  plusffval  18120  grpsubfval  18411  mulgfval  18490  sylow1lem2  18988  sylow2blem1  19009  sylow2blem2  19010  sylow3lem1  19016  sylow3lem6  19021  dmdprd  19385  dprdval  19390  staffval  19883  scaffval  19917  lpival  20283  ipffval  20610  cmpsub  22297  2ndcsep  22356  1stckgen  22451  kgencn2  22454  txcmplem1  22538  blbas  23328  met1stc  23419  psmetutop  23465  nmfval  23486  dchrptlem2  26146  dchrptlem3  26147  ishpg  26850  edgval  27140  bafval  28685  vsfval  28714  foresf1o  30569  fnpreimac  30728  nsgmgc  31311  nsgqusf1o  31315  idlsrgtset  31367  locfinreflem  31504  cmpcref  31514  rspectopn  31531  ordtconnlem1  31588  qqhval  31636  sigapildsys  31842  dya2icoseg2  31957  dya2iocuni  31962  sxbrsigalem2  31965  sxbrsigalem5  31967  omssubadd  31979  mvtval  33175  mvrsval  33180  mstaval  33219  brrestrict  33988  relowlssretop  35271  exrecfnlem  35287  ctbssinf  35314  lindsdom  35508  indexdom  35629  heiborlem1  35706  isdrngo2  35853  isrngohom  35860  idlval  35908  isidl  35909  igenval  35956  lsatset  36741  dicval  38927  trclexi  40904  rtrclexi  40905  dfrtrcl5  40913  dfrcl2  40959  stoweidlem59  43275  fourierdlem71  43393  salgensscntex  43558  aacllem  46176