Metamath Proof Explorer

Theorem eleqvrels2

Description: Element of the class of equivalence relations. (Contributed by Peter Mazsa, 24-Aug-2021)

Ref Expression
Assertion eleqvrels2 
|- ( R e. EqvRels <-> ( ( ( _I |` dom R ) C_ R /\ `' R C_ R /\ ( R o. R ) C_ R ) /\ R e. Rels ) )

Proof

Step Hyp Ref Expression
1 dfeqvrels2 
 |-  EqvRels = { r e. Rels | ( ( _I |` dom r ) C_ r /\ `' r C_ r /\ ( r o. 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 coideq 
 |-  ( r = R -> ( r o. r ) = ( R o. R ) )
9 8 4 sseq12d 
 |-  ( r = R -> ( ( r o. r ) C_ r <-> ( R o. R ) C_ R ) )
10 5 7 9 3anbi123d 
 |-  ( r = R -> ( ( ( _I |` dom r ) C_ r /\ `' r C_ r /\ ( r o. r ) C_ r ) <-> ( ( _I |` dom R ) C_ R /\ `' R C_ R /\ ( R o. R ) C_ R ) ) )
11 1 10 rabeqel 
 |-  ( R e. EqvRels <-> ( ( ( _I |` dom R ) C_ R /\ `' R C_ R /\ ( R o. R ) C_ R ) /\ R e. Rels ) )