Theorem coires1 6266

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

This proof depends on syntax axioms:   = wceq 1570   I cid 5555  ^◡ccnv 5660   ↾ cres 5663   ∘ ccom 5665  Rel wrel 5666

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5257  ax-pr 5404

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673

This theorem is used by:  relcoi1  6279  funcoeqres  6852  f1ofvswap  7304  relexpaddg  15095  funcrngcsetcALT  20749  lindfres  21982  lindsmm  21987  psrass1lem  22092  kgencn2  23723  ustssco  24381  symgcom  33412  cycpmconjv  33471  cycpmconjslem1  33483  erdsze2lem2  35704  poimirlem9  38308  mzpresrename  43509  diophrw  43518  eldioph2  43521  diophren  43568  relexpiidm  44458  relexpaddss  44472  cotrclrcl  44496  itcoval1  49471