This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )