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

Theorem rncoss 5958
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 5956 . 2 dom (𝐵𝐴) ⊆ dom 𝐴
2 df-rn 5663 . . 3 ran (𝐴𝐵) = dom (𝐴𝐵)
3 cnvco 5866 . . . 4 (𝐴𝐵) = (𝐵𝐴)
43dmeqi 5885 . . 3 dom (𝐴𝐵) = dom (𝐵𝐴)
52, 4eqtri 2788 . 2 ran (𝐴𝐵) = dom (𝐵𝐴)
6 df-rn 5663 . 2 ran 𝐴 = dom 𝐴
71, 5, 63sstr4i 3990 1 ran (𝐴𝐵) ⊆ ran 𝐴
Colors of variables: wff setvar class
Syntax hints:  wss 3907  ccnv 5651  dom cdm 5652  ran crn 5653  ccom 5656
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 5251  ax-pr 5395
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 5106  df-opab 5168  df-cnv 5660  df-co 5661  df-dm 5662  df-rn 5663
This theorem is referenced by:  cossxp  6263  fcof  6719  fin23lem29  10313  fin23lem30  10314  wunco  10706  imasless  17584  gsumzf1o  19973  znleval  21664  pi1xfrcnvlem  25176  pjss1coi  32424  pj3i  32469  smatrcl  34103  mblfinlem3  38170  mblfinlem4  38171  ismblfin  38172  relexp0a  44304  rntrclfv  44320  stoweidlem27  46599  fourierdlem42  46721  hoicvr  47120
  Copyright terms: Public domain W3C validator