Description: Composition with the identity relation restricted to a relation's field. (Contributed by FL, 2-May-2011)
Ref | Expression | ||
---|---|---|---|
Assertion | relcoi2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dmrnssfld | |
|
2 | unss | |
|
3 | simpr | |
|
4 | 2 3 | sylbir | |
5 | cores | |
|
6 | 1 4 5 | mp2b | |
7 | coi2 | |
|
8 | 6 7 | eqtrid | |