Theorem rnex 7886

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

Syntax hints:   ∈ wcel 2109  Vcvv 3447  ran crn 5639

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-cnv 5646  df-dm 5648  df-rn 5649

This theorem is referenced by:  elxp4  7898  elxp5  7899  ffoss  7924  fvclex  7937  wemoiso2  7953  2ndval  7971  fo2nd  7989  mapfoss  8825  ixpsnf1o  8911  bren  8928  mapen  9105  ssenen  9115  sucdom2  9167  fodomfib  9280  fodomfibOLD  9282  hartogslem1  9495  brwdom  9520  unxpwdom2  9541  noinfep  9613  r0weon  9965  fseqen  9980  acnlem  10001  infpwfien  10015  aceq3lem  10073  dfac4  10075  dfac5  10082  dfac2b  10084  dfac9  10090  dfac12lem2  10098  dfac12lem3  10099  infmap2  10170  cfflb  10212  infpssr  10261  fin23lem14  10286  fin23lem16  10288  fin23lem17  10291  fin23lem38  10302  fin23lem39  10303  axdc2lem  10401  axdc3lem2  10404  axcclem  10410  ttukeylem6  10467  wunex2  10691  wuncval2  10700  intgru  10767  wfgru  10769  qexALT  12923  seqexw  13982  shftfval  15036  vdwapval  16944  restfn  17387  prdsvallem  17417  prdsval  17418  wunfunc  17863  wunnat  17921  arwval  18005  catcfuccl  18080  catcxpccl  18168  yon11  18225  yon12  18226  yon2  18227  yonpropd  18229  oppcyon  18230  yonffth  18245  yoniso  18246  plusffval  18573  grpsubfval  18915  mulgfval  19001  sylow1lem2  19529  sylow2blem1  19550  sylow2blem2  19551  sylow3lem1  19557  sylow3lem6  19562  dmdprd  19930  dprdval  19935  staffval  20750  scaffval  20786  lpival  21234  ipffval  21557  cmpsub  23287  2ndcsep  23346  1stckgen  23441  kgencn2  23444  txcmplem1  23528  blbas  24318  met1stc  24409  psmetutop  24455  nmfval  24476  dchrptlem2  27176  dchrptlem3  27177  mulsproplem9  28027  ishpg  28686  edgval  28976  bafval  30533  vsfval  30562  foresf1o  32433  fnpreimac  32595  nsgmgc  33383  nsgqusf1o  33387  idlsrgtset  33479  locfinreflem  33830  cmpcref  33840  rspectopn  33857  ordtconnlem1  33914  qqhval  33962  sigapildsys  34152  dya2icoseg2  34269  dya2iocuni  34274  sxbrsigalem2  34277  sxbrsigalem5  34279  omssubadd  34291  mvtval  35487  mvrsval  35492  mstaval  35531  brrestrict  35937  relowlssretop  37351  exrecfnlem  37367  ctbssinf  37394  lindsdom  37608  indexdom  37728  heiborlem1  37805  isdrngo2  37952  isrngohom  37959  idlval  38007  isidl  38008  igenval  38055  lsatset  38983  dicval  41170  aks6d1c6isolem2  42163  prjcrvfval  42619  trclexi  43609  rtrclexi  43610  dfrtrcl5  43618  dfrcl2  43663  wfaxrep  44984  stoweidlem59  46057  fourierdlem71  46175  salgensscntex  46342  aacllem  49790