MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rncoss Structured version   Visualization version   GIF version

Theorem rncoss 5957
Description: Range of a composition. (Contributed by NM, 19-Mar-1998.)
Assertion
Ref Expression
rncoss ran (𝐴𝐵) ⊆ ran 𝐴

Proof of Theorem rncoss
StepHypRef Expression
1 dmcoss 5955 . 2 dom (𝐵𝐴) ⊆ dom 𝐴
2 df-rn 5662 . . 3 ran (𝐴𝐵) = dom (𝐴𝐵)
3 cnvco 5865 . . . 4 (𝐴𝐵) = (𝐵𝐴)
43dmeqi 5884 . . 3 dom (𝐴𝐵) = dom (𝐵𝐴)
52, 4eqtri 2788 . 2 ran (𝐴𝐵) = dom (𝐵𝐴)
6 df-rn 5662 . 2 ran 𝐴 = dom 𝐴
71, 5, 63sstr4i 3990 1 ran (𝐴𝐵) ⊆ ran 𝐴
Colors of variables: wff setvar class
Syntax hints:  wss 3907  ccnv 5650  dom cdm 5651  ran crn 5652  ccom 5655
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5250  ax-pr 5394
This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5105  df-opab 5167  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662
This theorem is referenced by:  cossxp  6262  fcof  6719  fin23lem29  10313  fin23lem30  10314  wunco  10706  imasless  17582  gsumzf1o  19970  znleval  21661  pi1xfrcnvlem  25172  pjss1coi  32420  pj3i  32465  smatrcl  34098  mblfinlem3  38165  mblfinlem4  38166  ismblfin  38167  relexp0a  44299  rntrclfv  44315  stoweidlem27  46600  fourierdlem42  46722  hoicvr  47121
  Copyright terms: Public domain W3C validator