Theorem rnex 7920

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

This proof depends on syntax axioms:   ∈ wcel 2145  Vcvv 3451  ran crn 5652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391  ax-un 7749

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-cnv 5659  df-dm 5661  df-rn 5662

This theorem is used by:  elxp4  7932  elxp5  7933  ffoss  7956  fvclex  7969  wemoiso2  7984  2ndval  8002  fo2nd  8020  mapfoss  8867  ixpsnf1o  8959  bren  8976  mapen  9153  ssenen  9163  sucdom2  9211  fodomfib  9313  hartogslem1  9529  brwdom  9554  unxpwdom2  9575  noinfep  9654  r0weon  10084  fseqen  10099  acnlem  10120  infpwfien  10134  aceq3lem  10192  dfac4  10194  dfac5  10200  dfac2b  10202  dfac9  10208  dfac12lem2  10216  dfac12lem3  10217  infmap2  10288  cfflb  10330  infpssr  10379  fin23lem14  10404  fin23lem16  10406  fin23lem17  10409  fin23lem38  10420  fin23lem39  10421  axdc2lem  10519  axdc3lem2  10522  axcclem  10528  ttukeylem6  10585  wunex2  10816  wuncval2  10825  intgru  10892  wfgru  10894  qexALT  13084  seqexw  14153  shftfval  15216  vdwapval  17144  restfn  17588  prdsvallem  17618  prdsval  17619  wunfunc  18069  wunnat  18127  arwval  18211  catcfuccl  18286  catcxpccl  18374  yon11  18431  yon12  18432  yon2  18433  yonpropd  18435  oppcyon  18436  yonffth  18451  yoniso  18452  plusffval  18815  grpsubfval  19187  mulgfval  19272  sylow1lem2  19806  sylow2blem1  19827  sylow2blem2  19828  sylow3lem1  19834  sylow3lem6  19839  dmdprd  20207  dprdval  20212  staffval  21091  scaffval  21148  lpival  21641  ipffval  21947  lindsdom  22149  cmpsub  23711  2ndcsep  23771  1stckgen  23866  kgencn2  23869  txcmplem1  23953  blbas  24742  met1stc  24833  psmetutop  24879  nmfval  24900  dchrptlem2  27585  dchrptlem3  27586  mulsproplem9  28503  ishpg  29230  tgplnfn  29246  plngval  29248  isplng  29249  brprlng  29409  edgval  29620  bafval  31199  vsfval  31228  foresf1o  33093  fnpreimac  33257  nsgmgc  33956  nsgqusf1o  33960  idlsrgtset  34033  locfinreflem  34465  cmpcref  34475  rspectopn  34492  ordtconnlem1  34549  qqhval  34597  sigapildsys  34788  dya2icoseg2  34903  dya2iocuni  34908  sxbrsigalem2  34911  sxbrsigalem5  34913  omssubadd  34925  mvtval  36244  mvrsval  36249  mstaval  36288  brrestrict  36693  relowlssretop  38266  exrecfnlem  38282  ctbssinf  38309  indexdom  38648  heiborlem1  38725  isdrngo2  38872  isrngohom  38879  idlval  38927  isidl  38928  igenval  38975  lsatset  40027  dicval  42213  aks6d1c6isolem2  43205  prjcrvfval  43647  trclexi  44605  rtrclexi  44606  dfrtrcl5  44614  dfrcl2  44659  wfaxrep  45962  stoweidlem59  47038  fourierdlem71  47156  salgensscntex  47323  aacllem  50908