Metamath Proof Explorer

Theorem dfeqvrel2

Description: Alternate definition of the equivalence relation predicate. (Contributed by Peter Mazsa, 22-Apr-2019)

Ref Expression
Assertion dfeqvrel2 
|- ( EqvRel R <-> ( ( ( _I |` dom R ) C_ R /\ `' R C_ R /\ ( R o. R ) C_ R ) /\ Rel R ) )

Proof

Step Hyp Ref Expression
1 df-eqvrel 
 |-  ( EqvRel R <-> ( RefRel R /\ SymRel R /\ TrRel R ) )
2 refsymrel2 
 |-  ( ( RefRel R /\ SymRel R ) <-> ( ( ( _I |` dom R ) C_ R /\ `' R C_ R ) /\ Rel R ) )
3 dftrrel2 
 |-  ( TrRel R <-> ( ( R o. R ) C_ R /\ Rel R ) )
4 2 3 anbi12i 
 |-  ( ( ( RefRel R /\ SymRel R ) /\ TrRel R ) <-> ( ( ( ( _I |` dom R ) C_ R /\ `' R C_ R ) /\ Rel R ) /\ ( ( R o. R ) C_ R /\ Rel R ) ) )
5 df-3an 
 |-  ( ( RefRel R /\ SymRel R /\ TrRel R ) <-> ( ( RefRel R /\ SymRel R ) /\ TrRel R ) )
6 df-3an 
 |-  ( ( ( _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 ) )
7 6 anbi1i 
 |-  ( ( ( ( _I |` dom R ) C_ R /\ `' R C_ R /\ ( R o. R ) C_ R ) /\ Rel R ) <-> ( ( ( ( _I |` dom R ) C_ R /\ `' R C_ R ) /\ ( R o. R ) C_ R ) /\ Rel R ) )
8 3anan32 
 |-  ( ( ( ( _I |` dom R ) C_ R /\ `' R C_ R ) /\ Rel R /\ ( R o. R ) C_ R ) <-> ( ( ( ( _I |` dom R ) C_ R /\ `' R C_ R ) /\ ( R o. R ) C_ R ) /\ Rel R ) )
9 anandi3r 
 |-  ( ( ( ( _I |` dom R ) C_ R /\ `' R C_ R ) /\ Rel R /\ ( R o. R ) C_ R ) <-> ( ( ( ( _I |` dom R ) C_ R /\ `' R C_ R ) /\ Rel R ) /\ ( ( R o. R ) C_ R /\ Rel R ) ) )
10 7 8 9 3bitr2i 
 |-  ( ( ( ( _I |` dom R ) C_ R /\ `' R C_ R /\ ( R o. R ) C_ R ) /\ Rel R ) <-> ( ( ( ( _I |` dom R ) C_ R /\ `' R C_ R ) /\ Rel R ) /\ ( ( R o. R ) C_ R /\ Rel R ) ) )
11 4 5 10 3bitr4i 
 |-  ( ( RefRel R /\ SymRel R /\ TrRel R ) <-> ( ( ( _I |` dom R ) C_ R /\ `' R C_ R /\ ( R o. R ) C_ R ) /\ Rel R ) )
12 1 11 bitri 
 |-  ( EqvRel R <-> ( ( ( _I |` dom R ) C_ R /\ `' R C_ R /\ ( R o. R ) C_ R ) /\ Rel R ) )