Theorem rnex 7924

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

This proof depends on syntax axioms:   ∈ wcel 2144  Vcvv 3450  ran crn 5651

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390  ax-un 7753

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-cnv 5658  df-dm 5660  df-rn 5661

This theorem is used by:  elxp4  7936  elxp5  7937  ffoss  7960  fvclex  7973  wemoiso2  7988  2ndval  8006  fo2nd  8024  mapfoss  8879  ixpsnf1o  8971  bren  8988  mapen  9165  ssenen  9175  sucdom2  9223  fodomfib  9325  hartogslem1  9541  brwdom  9566  unxpwdom2  9587  noinfep  9666  r0weon  10096  fseqen  10111  acnlem  10132  infpwfien  10146  aceq3lem  10204  dfac4  10206  dfac5  10212  dfac2b  10214  dfac9  10220  dfac12lem2  10228  dfac12lem3  10229  infmap2  10300  cfflb  10342  infpssr  10391  fin23lem14  10416  fin23lem16  10418  fin23lem17  10421  fin23lem38  10432  fin23lem39  10433  axdc2lem  10531  axdc3lem2  10534  axcclem  10540  ttukeylem6  10597  wunex2  10828  wuncval2  10837  intgru  10904  wfgru  10906  qexALT  13096  seqexw  14165  shftfval  15230  vdwapval  17158  restfn  17602  prdsvallem  17632  prdsval  17633  wunfunc  18083  wunnat  18141  arwval  18225  catcfuccl  18300  catcxpccl  18388  yon11  18445  yon12  18446  yon2  18447  yonpropd  18449  oppcyon  18450  yonffth  18465  yoniso  18466  plusffval  18829  grpsubfval  19201  mulgfval  19286  sylow1lem2  19820  sylow2blem1  19841  sylow2blem2  19842  sylow3lem1  19848  sylow3lem6  19853  dmdprd  20221  dprdval  20226  staffval  21105  scaffval  21162  lpival  21655  ipffval  21961  lindsdom  22163  cmpsub  23725  2ndcsep  23785  1stckgen  23880  kgencn2  23883  txcmplem1  23967  blbas  24756  met1stc  24847  psmetutop  24893  nmfval  24914  dchrptlem2  27599  dchrptlem3  27600  mulsproplem9  28517  ishpg  29244  tgplnfn  29260  plngval  29262  isplng  29263  brprlng  29423  edgval  29634  bafval  31213  vsfval  31242  foresf1o  33149  fnpreimac  33313  nsgmgc  34011  nsgqusf1o  34015  idlsrgtset  34088  locfinreflem  34520  rspectopn  34547  ordtconnlem1  34604  qqhval  34652  sigapildsys  34843  dya2icoseg2  34958  dya2iocuni  34963  sxbrsigalem2  34966  sxbrsigalem5  34968  omssubadd  34980  mvtval  36353  mvrsval  36358  mstaval  36397  brrestrict  36807  relowlssretop  38393  exrecfnlem  38409  ctbssinf  38436  indexdom  38775  heiborlem1  38852  isdrngo2  38999  isrngohom  39006  idlval  39054  isidl  39055  igenval  39102  lsatset  40154  dicval  42340  aks6d1c6isolem2  43332  prjcrvfval  43774  trclexi  44727  rtrclexi  44728  dfrtrcl5  44736  dfrcl2  44781  wfaxrep  46091  stoweidlem59  47176  fourierdlem71  47294  salgensscntex  47461  aacllem  51121