Metamath Proof Explorer


Theorem refrelcoss2

Description: The class of cosets by R is reflexive, see dfrefrel2 . (Contributed by Peter Mazsa, 30-Jul-2019)

Ref Expression
Assertion refrelcoss2 IdomR×ranRRRelR

Proof

Step Hyp Ref Expression
1 refrelcoss3 xdomRyranRx=yxRyRelR
2 idinxpss IdomR×ranRRxdomRyranRx=yxRy
3 2 anbi1i IdomR×ranRRRelRxdomRyranRx=yxRyRelR
4 1 3 mpbir IdomR×ranRRRelR