Metamath Proof Explorer

Theorem elrefsymrels2

Description: Elements of the class of reflexive relations which are elements of the class of symmetric relations as well (like the elements of the class of equivalence relations dfeqvrels2 ) can use the restricted version for their reflexive part (see below), not just the (I i^i ( dom R X. ran R ) ) C R version of dfrefrels2 , cf. the comment of dfrefrels2 . (Contributed by Peter Mazsa, 22-Jul-2019)

Ref Expression
Assertion elrefsymrels2 
|- ( R e. ( RefRels i^i SymRels ) <-> ( ( ( _I |` dom R ) C_ R /\ `' R C_ R ) /\ R e. Rels ) )

Proof

Step Hyp Ref Expression
1 refsymrels2 
 |-  ( RefRels i^i SymRels ) = { r e. Rels | ( ( _I |` dom r ) C_ r /\ `' r C_ r ) }
2 dmeq 
 |-  ( r = R -> dom r = dom R )
3 2 reseq2d 
 |-  ( r = R -> ( _I |` dom r ) = ( _I |` dom R ) )
4 id 
 |-  ( r = R -> r = R )
5 3 4 sseq12d 
 |-  ( r = R -> ( ( _I |` dom r ) C_ r <-> ( _I |` dom R ) C_ R ) )
6 cnveq 
 |-  ( r = R -> `' r = `' R )
7 6 4 sseq12d 
 |-  ( r = R -> ( `' r C_ r <-> `' R C_ R ) )
8 5 7 anbi12d 
 |-  ( r = R -> ( ( ( _I |` dom r ) C_ r /\ `' r C_ r ) <-> ( ( _I |` dom R ) C_ R /\ `' R C_ R ) ) )
9 1 8 rabeqel 
 |-  ( R e. ( RefRels i^i SymRels ) <-> ( ( ( _I |` dom R ) C_ R /\ `' R C_ R ) /\ R e. Rels ) )