Theorem rnex 6992

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

Syntax hints:   ∈ wcel 1977  Vcvv 3173  ran crn 5039

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-rab 2905  df-v 3175  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-cnv 5046  df-dm 5048  df-rn 5049

This theorem is referenced by:  elxp4  7003  elxp5  7004  ffoss  7020  fvclex  7031  abrexex  7033  wemoiso2  7045  2ndval  7062  fo2nd  7080  ixpsnf1o  7834  bren  7850  mapen  8009  ssenen  8019  sucdom2  8041  fodomfib  8125  hartogslem1  8330  brwdom  8355  unxpwdom2  8376  noinfep  8440  r0weon  8718  fseqen  8733  acnlem  8754  infpwfien  8768  aceq3lem  8826  dfac4  8828  dfac5  8834  dfac2  8836  dfac9  8841  dfac12lem2  8849  dfac12lem3  8850  infmap2  8923  cfflb  8964  infpssr  9013  fin23lem14  9038  fin23lem16  9040  fin23lem17  9043  fin23lem38  9054  fin23lem39  9055  axdc2lem  9153  axdc3lem2  9156  axcclem  9162  ttukeylem6  9219  wunex2  9439  wuncval2  9448  intgru  9515  wfgru  9517  qexALT  11679  hashfacen  13095  shftfval  13658  vdwapval  15515  restfn  15908  prdsval  15938  wunfunc  16382  wunnat  16439  arwval  16516  catcfuccl  16582  catcxpccl  16670  yon11  16727  yon12  16728  yon2  16729  yonpropd  16731  oppcyon  16732  yonffth  16747  yoniso  16748  plusffval  17070  sylow1lem2  17837  sylow2blem1  17858  sylow2blem2  17859  sylow3lem1  17865  sylow3lem6  17870  dmdprd  18220  dprdval  18225  staffval  18670  scaffval  18704  lpival  19066  ipffval  19812  cmpsub  21013  2ndcsep  21072  1stckgen  21167  kgencn2  21170  txcmplem1  21254  blbas  22045  met1stc  22136  psmetutop  22182  nmfval  22203  qtopbaslem  22372  dchrptlem2  24790  dchrptlem3  24791  ishpg  25451  edgaval  25794  edgval  25868  bafval  26843  vsfval  26872  foresf1o  28727  locfinreflem  29235  cmpcref  29245  ordtconlem1  29298  qqhval  29346  sigapildsys  29552  dya2icoseg2  29667  dya2iocuni  29672  sxbrsigalem2  29675  sxbrsigalem5  29677  omssubadd  29689  mvtval  30651  mvrsval  30656  mstaval  30695  trpredex  30981  brrestrict  31226  relowlssretop  32387  lindsdom  32573  indexdom  32699  heiborlem1  32780  isdrngo2  32927  isrngohom  32934  idlval  32982  isidl  32983  igenval  33030  lsatset  33295  dicval  35483  trclexi  36946  rtrclexi  36947  dfrtrcl5  36955  dfrcl2  36985  stoweidlem59  38952  fourierdlem71  39070  salgensscntex  39238  aacllem  42356