Theorem coires1 6237

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

Step	Hyp	Ref	Expression
1		cocnvcnv1 6230	. . . . 5 ⊢ (◡◡𝐴 ∘ I ) = (𝐴 ∘ I )
2		relcnv 6075	. . . . . 6 ⊢ Rel ◡◡𝐴
3		coi1 6235	. . . . . 6 ⊢ (Rel ◡◡𝐴 → (◡◡𝐴 ∘ I ) = ◡◡𝐴)
4	2, 3	ax-mp 5	. . . . 5 ⊢ (◡◡𝐴 ∘ I ) = ◡◡𝐴
5	1, 4	eqtr3i 2754	. . . 4 ⊢ (𝐴 ∘ I ) = ◡◡𝐴
6	5	reseq1i 5946	. . 3 ⊢ ((𝐴 ∘ I ) ↾ 𝐵) = (◡◡𝐴 ↾ 𝐵)
7		resco 6223	. . 3 ⊢ ((𝐴 ∘ I ) ↾ 𝐵) = (𝐴 ∘ ( I ↾ 𝐵))
8	6, 7	eqtr3i 2754	. 2 ⊢ (◡◡𝐴 ↾ 𝐵) = (𝐴 ∘ ( I ↾ 𝐵))
9		rescnvcnv 6177	. 2 ⊢ (◡◡𝐴 ↾ 𝐵) = (𝐴 ↾ 𝐵)
10	8, 9	eqtr3i 2754	1 ⊢ (𝐴 ∘ ( I ↾ 𝐵)) = (𝐴 ↾ 𝐵)

Syntax hints:   = wceq 1540   I cid 5532  ^◡ccnv 5637   ↾ cres 5640   ∘ ccom 5642  Rel wrel 5643

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650

This theorem is referenced by:  relcoi1  6251  funcoeqres  6831  f1ofvswap  7281  relexpaddg  15019  funcrngcsetcALT  20550  lindfres  21732  lindsmm  21737  psrass1lem  21841  kgencn2  23444  ustssco  24102  symgcom  33040  cycpmconjv  33099  cycpmconjslem1  33111  erdsze2lem2  35191  poimirlem9  37623  mzpresrename  42738  diophrw  42747  eldioph2  42750  diophren  42801  relexpiidm  43693  relexpaddss  43707  cotrclrcl  43731  itcoval1  48652