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

Theorem rncoss 5963
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 5962 . 2 dom (𝐵𝐴) ⊆ dom 𝐴
2 df-rn 5680 . . 3 ran (𝐴𝐵) = dom (𝐴𝐵)
3 cnvco 5877 . . . 4 (𝐴𝐵) = (𝐵𝐴)
43dmeqi 5896 . . 3 dom (𝐴𝐵) = dom (𝐵𝐴)
52, 4eqtri 2759 . 2 ran (𝐴𝐵) = dom (𝐵𝐴)
6 df-rn 5680 . 2 ran 𝐴 = dom 𝐴
71, 5, 63sstr4i 4021 1 ran (𝐴𝐵) ⊆ ran 𝐴
Colors of variables: wff setvar class
Syntax hints:  wss 3944  ccnv 5668  dom cdm 5669  ran crn 5670  ccom 5673
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-12 2171  ax-ext 2702  ax-sep 5292  ax-nul 5299  ax-pr 5420
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-sn 4623  df-pr 4625  df-op 4629  df-br 5142  df-opab 5204  df-cnv 5677  df-co 5678  df-dm 5679  df-rn 5680
This theorem is referenced by:  cossxp  6260  fcof  6727  fcoOLD  6729  fco3OLD  6738  fin23lem29  10318  fin23lem30  10319  wunco  10710  imasless  17468  gsumzf1o  19739  znleval  21043  pi1xfrcnvlem  24501  pjss1coi  31279  pj3i  31324  smatrcl  32607  mblfinlem3  36331  mblfinlem4  36332  ismblfin  36333  relexp0a  42238  rntrclfv  42254  stoweidlem27  44516  fourierdlem42  44638  hoicvr  45037
  Copyright terms: Public domain W3C validator