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 i^i ( dom ,~ R X. ran ,~ R ) ) C_ ,~ R /\ Rel ,~ R )

Proof

Step	Hyp	Ref	Expression
1		refrelcoss3	|- ( A. x e. dom ,~ R A. y e. ran ,~ R ( x = y -> x ,~ R y ) /\ Rel ,~ R )
2		idinxpss	|- ( ( _I i^i ( dom ,~ R X. ran ,~ R ) ) C_ ,~ R <-> A. x e. dom ,~ R A. y e. ran ,~ R ( x = y -> x ,~ R y ) )
3	2	anbi1i	|- ( ( ( _I i^i ( dom ,~ R X. ran ,~ R ) ) C_ ,~ R /\ Rel ,~ R ) <-> ( A. x e. dom ,~ R A. y e. ran ,~ R ( x = y -> x ,~ R y ) /\ Rel ,~ R ) )
4	1 3	mpbir	|- ( ( _I i^i ( dom ,~ R X. ran ,~ R ) ) C_ ,~ R /\ Rel ,~ R )