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

Theorem coires1 5956
Description: Composition with a restricted identity relation. (Contributed by FL, 19-Jun-2011.) (Revised by Stefan O'Rear, 7-Mar-2015.)
Assertion
Ref Expression
coires1 (𝐴 ∘ ( I ↾ 𝐵)) = (𝐴𝐵)

Proof of Theorem coires1
StepHypRef Expression
1 cocnvcnv1 5949 . . . . 5 (𝐴 ∘ I ) = (𝐴 ∘ I )
2 relcnv 5807 . . . . . 6 Rel 𝐴
3 coi1 5954 . . . . . 6 (Rel 𝐴 → (𝐴 ∘ I ) = 𝐴)
42, 3ax-mp 5 . . . . 5 (𝐴 ∘ I ) = 𝐴
51, 4eqtr3i 2804 . . . 4 (𝐴 ∘ I ) = 𝐴
65reseq1i 5691 . . 3 ((𝐴 ∘ I ) ↾ 𝐵) = (𝐴𝐵)
7 resco 5942 . . 3 ((𝐴 ∘ I ) ↾ 𝐵) = (𝐴 ∘ ( I ↾ 𝐵))
86, 7eqtr3i 2804 . 2 (𝐴𝐵) = (𝐴 ∘ ( I ↾ 𝐵))
9 rescnvcnv 5900 . 2 (𝐴𝐵) = (𝐴𝐵)
108, 9eqtr3i 2804 1 (𝐴 ∘ ( I ↾ 𝐵)) = (𝐴𝐵)
Colors of variables: wff setvar class
Syntax hints:   = wceq 1507   I cid 5311  ccnv 5406  cres 5409  ccom 5411  Rel wrel 5412
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5060  ax-nul 5067  ax-pr 5186
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-dif 3832  df-un 3834  df-in 3836  df-ss 3843  df-nul 4179  df-if 4351  df-sn 4442  df-pr 4444  df-op 4448  df-br 4930  df-opab 4992  df-id 5312  df-xp 5413  df-rel 5414  df-cnv 5415  df-co 5416  df-dm 5417  df-rn 5418  df-res 5419
This theorem is referenced by:  relcoi1  5967  funcoeqres  6474  relexpaddg  14273  psrass1lem  19871  lindfres  20669  lindsmm  20674  kgencn2  21869  ustssco  22526  erdsze2lem2  32042  poimirlem9  34348  mzpresrename  38748  diophrw  38757  eldioph2  38760  diophren  38812  relexpiidm  39418  relexpaddss  39432  cotrclrcl  39456  funcrngcsetcALT  43640
  Copyright terms: Public domain W3C validator