Theorem coires1 6273

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 6266	. . . . 5 ⊢ (◡◡𝐴 ∘ I ) = (𝐴 ∘ I )
2		relcnv 6106	. . . . . 6 ⊢ Rel ◡◡𝐴
3		coi1 6271	. . . . . 6 ⊢ (Rel ◡◡𝐴 → (◡◡𝐴 ∘ I ) = ◡◡𝐴)
4	2, 3	ax-mp 5	. . . . 5 ⊢ (◡◡𝐴 ∘ I ) = ◡◡𝐴
5	1, 4	eqtr3i 2788	. . . 4 ⊢ (𝐴 ∘ I ) = ◡◡𝐴
6	5	reseq1i 5971	. . 3 ⊢ ((𝐴 ∘ I ) ↾ 𝐵) = (◡◡𝐴 ↾ 𝐵)
7		resco 6258	. . 3 ⊢ ((𝐴 ∘ I ) ↾ 𝐵) = (𝐴 ∘ ( I ↾ 𝐵))
8	6, 7	eqtr3i 2788	. 2 ⊢ (◡◡𝐴 ↾ 𝐵) = (𝐴 ∘ ( I ↾ 𝐵))
9		rescnvcnv 6212	. 2 ⊢ (◡◡𝐴 ↾ 𝐵) = (𝐴 ↾ 𝐵)
10	8, 9	eqtr3i 2788	1 ⊢ (𝐴 ∘ ( I ↾ 𝐵)) = (𝐴 ↾ 𝐵)

This proof depends on syntax axioms:   = wceq 1569   I cid 5549  ^◡ccnv 5654   ↾ cres 5657   ∘ ccom 5659  Rel wrel 5660

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735  ax-sep 5252  ax-pr 5395

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667

This theorem is used by:  relcoi1  6288  funcoeqres  6867  f1ofvswap  7324  relexpaddg  15221  funcrngcsetcALT  20908  lindfres  22144  lindsmm  22149  psrass1lem  22256  kgencn2  23891  ustssco  24549  symgcom  33700  cycpmconjv  33759  cycpmconjslem1  33771  erdsze2lem2  36093  poimirlem9  38693  mzpresrename  43907  diophrw  43916  eldioph2  43919  diophren  43966  relexpiidm  44850  relexpaddss  44864  cotrclrcl  44888  itcoval1  49920