Theorem elcnvrefrels2

Description: Element of the class of converse reflexive relations. (Contributed by Peter Mazsa, 25-Jul-2019)

	Ref	Expression
Assertion	elcnvrefrels2	|- ( R e. CnvRefRels <-> ( R C_ ( _I i^i ( dom R X. ran R ) ) /\ R e. Rels ) )

Proof

Step	Hyp	Ref	Expression
1		dfcnvrefrels2	|- CnvRefRels = { r e. Rels | r C_ ( _I i^i ( dom r X. ran r ) ) }
2		id	|- ( r = R -> r = R )
3		dmeq	|- ( r = R -> dom r = dom R )
4		rneq	|- ( r = R -> ran r = ran R )
5	3 4	xpeq12d	|- ( r = R -> ( dom r X. ran r ) = ( dom R X. ran R ) )
6	5	ineq2d	|- ( r = R -> ( _I i^i ( dom r X. ran r ) ) = ( _I i^i ( dom R X. ran R ) ) )
7	2 6	sseq12d	|- ( r = R -> ( r C_ ( _I i^i ( dom r X. ran r ) ) <-> R C_ ( _I i^i ( dom R X. ran R ) ) ) )
8	1 7	rabeqel	|- ( R e. CnvRefRels <-> ( R C_ ( _I i^i ( dom R X. ran R ) ) /\ R e. Rels ) )