Metamath Proof Explorer

Theorem refrelcoss

Description: The class of cosets by R is reflexive. (Contributed by Peter Mazsa, 4-Jul-2020)

Ref Expression
Assertion refrelcoss 
|- RefRel ,~ R

Proof

Step Hyp Ref Expression
1 refrelcoss2 
 |-  ( ( _I i^i ( dom ,~ R X. ran ,~ R ) ) C_ ,~ R /\ Rel ,~ R )
2 dfrefrel2 
 |-  ( RefRel ,~ R <-> ( ( _I i^i ( dom ,~ R X. ran ,~ R ) ) C_ ,~ R /\ Rel ,~ R ) )
3 1 2 mpbir 
 |-  RefRel ,~ R