Metamath Proof Explorer


Theorem relcoi2

Description: Composition with the identity relation restricted to a relation's field. (Contributed by FL, 2-May-2011)

Ref Expression
Assertion relcoi2 RelRIRR=R

Proof

Step Hyp Ref Expression
1 dmrnssfld domRranRR
2 unss domRRranRRdomRranRR
3 simpr domRRranRRranRR
4 2 3 sylbir domRranRRranRR
5 cores ranRRIRR=IR
6 1 4 5 mp2b IRR=IR
7 coi2 RelRIR=R
8 6 7 eqtrid RelRIRR=R