Metamath Proof Explorer

Theorem elrefrels2

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

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

Proof

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