Theorem rnex 7956

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

This proof depends on syntax axioms:   ∈ wcel 2147  Vcvv 3454  ran crn 5659

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5255  ax-pr 5398  ax-un 7783

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-cnv 5666  df-dm 5668  df-rn 5669

This theorem is used by:  elxp4  7968  elxp5  7969  ffoss  7992  fvclex  8005  wemoiso2  8020  2ndval  8038  fo2nd  8056  mapfoss  8912  ixpsnf1o  9004  bren  9021  mapen  9198  ssenen  9208  sucdom2  9256  fodomfib  9358  hartogslem1  9573  brwdom  9598  unxpwdom2  9619  noinfep  9698  r0weon  10130  fseqen  10145  acnlem  10166  infpwfien  10180  aceq3lem  10238  dfac4  10240  dfac5  10246  dfac2b  10248  dfac9  10254  dfac12lem2  10262  dfac12lem3  10263  infmap2  10334  cfflb  10376  infpssr  10425  fin23lem14  10450  fin23lem16  10452  fin23lem17  10455  fin23lem38  10466  fin23lem39  10467  axdc2lem  10565  axdc3lem2  10568  axcclem  10574  ttukeylem6  10631  wunex2  10862  wuncval2  10871  intgru  10938  wfgru  10940  qexALT  13131  seqexw  14200  shftfval  15266  vdwapval  17195  restfn  17645  prdsvallem  17675  prdsval  17676  wunfunc  18126  wunnat  18184  arwval  18268  catcfuccl  18343  catcxpccl  18431  yon11  18488  yon12  18489  yon2  18490  yonpropd  18492  oppcyon  18493  yonffth  18508  yoniso  18509  plusffval  18872  grpsubfval  19244  mulgfval  19329  sylow1lem2  19864  sylow2blem1  19885  sylow2blem2  19886  sylow3lem1  19892  sylow3lem6  19897  dmdprd  20265  dprdval  20270  staffval  21149  scaffval  21206  lpival  21699  ipffval  22009  lindsdom  22211  cmpsub  23773  2ndcsep  23833  1stckgen  23928  kgencn2  23931  txcmplem1  24015  blbas  24804  met1stc  24895  psmetutop  24941  nmfval  24962  dchrptlem2  27649  dchrptlem3  27650  mulsproplem9  28567  ishpg  29294  tgplnfn  29310  plngval  29312  isplng  29313  brprlng  29473  edgval  29684  bafval  31263  vsfval  31292  foresf1o  33199  fnpreimac  33362  nsgmgc  34067  nsgqusf1o  34071  idlsrgtset  34144  locfinreflem  34583  rspectopn  34610  ordtconnlem1  34667  qqhval  34715  sigapildsys  34906  dya2icoseg2  35021  dya2iocuni  35026  sxbrsigalem2  35029  sxbrsigalem5  35031  omssubadd  35043  mvtval  36473  mvrsval  36478  mstaval  36517  brrestrict  36928  relowlssretop  38554  exrecfnlem  38570  ctbssinf  38597  indexdom  38936  heiborlem1  39011  isdrngo2  39158  isrngohom  39165  idlval  39213  isidl  39214  igenval  39261  lsatset  40313  dicval  42499  aks6d1c6isolem2  43491  prjcrvfval  43933  trclexi  44881  rtrclexi  44882  dfrtrcl5  44890  dfrcl2  44935  wfaxrep  46248  stoweidlem59  47342  fourierdlem71  47460  salgensscntex  47627  aacllem  51367