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 I dom R × ran R R Rel R

Proof

Step Hyp Ref Expression
1 refrelcoss3 x dom R y ran R x = y x R y Rel R
2 idinxpss I dom R × ran R R x dom R y ran R x = y x R y
3 2 anbi1i I dom R × ran R R Rel R x dom R y ran R x = y x R y Rel R
4 1 3 mpbir I dom R × ran R R Rel R