Metamath Proof Explorer

Theorem dfeqvrel3

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

Ref Expression
Assertion dfeqvrel3 
|- ( EqvRel R <-> ( ( A. x e. dom R x R x /\ A. x A. y ( x R y -> y R x ) /\ A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) ) /\ Rel R ) )

Proof

Step Hyp Ref Expression
1 df-eqvrel 
 |-  ( EqvRel R <-> ( RefRel R /\ SymRel R /\ TrRel R ) )
2 refsymrel3 
 |-  ( ( RefRel R /\ SymRel R ) <-> ( ( A. x e. dom R x R x /\ A. x A. y ( x R y -> y R x ) ) /\ Rel R ) )
3 dftrrel3 
 |-  ( TrRel R <-> ( A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) /\ Rel R ) )
4 2 3 anbi12i 
 |-  ( ( ( RefRel R /\ SymRel R ) /\ TrRel R ) <-> ( ( ( A. x e. dom R x R x /\ A. x A. y ( x R y -> y R x ) ) /\ Rel R ) /\ ( A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) /\ Rel R ) ) )
5 df-3an 
 |-  ( ( RefRel R /\ SymRel R /\ TrRel R ) <-> ( ( RefRel R /\ SymRel R ) /\ TrRel R ) )
6 df-3an 
 |-  ( ( A. x e. dom R x R x /\ A. x A. y ( x R y -> y R x ) /\ A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) ) <-> ( ( A. x e. dom R x R x /\ A. x A. y ( x R y -> y R x ) ) /\ A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) ) )
7 6 anbi1i 
 |-  ( ( ( A. x e. dom R x R x /\ A. x A. y ( x R y -> y R x ) /\ A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) ) /\ Rel R ) <-> ( ( ( A. x e. dom R x R x /\ A. x A. y ( x R y -> y R x ) ) /\ A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) ) /\ Rel R ) )
8 3anan32 
 |-  ( ( ( A. x e. dom R x R x /\ A. x A. y ( x R y -> y R x ) ) /\ Rel R /\ A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) ) <-> ( ( ( A. x e. dom R x R x /\ A. x A. y ( x R y -> y R x ) ) /\ A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) ) /\ Rel R ) )
9 anandi3r 
 |-  ( ( ( A. x e. dom R x R x /\ A. x A. y ( x R y -> y R x ) ) /\ Rel R /\ A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) ) <-> ( ( ( A. x e. dom R x R x /\ A. x A. y ( x R y -> y R x ) ) /\ Rel R ) /\ ( A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) /\ Rel R ) ) )
10 7 8 9 3bitr2i 
 |-  ( ( ( A. x e. dom R x R x /\ A. x A. y ( x R y -> y R x ) /\ A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) ) /\ Rel R ) <-> ( ( ( A. x e. dom R x R x /\ A. x A. y ( x R y -> y R x ) ) /\ Rel R ) /\ ( A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) /\ Rel R ) ) )
11 4 5 10 3bitr4i 
 |-  ( ( RefRel R /\ SymRel R /\ TrRel R ) <-> ( ( A. x e. dom R x R x /\ A. x A. y ( x R y -> y R x ) /\ A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) ) /\ Rel R ) )
12 1 11 bitri 
 |-  ( EqvRel R <-> ( ( A. x e. dom R x R x /\ A. x A. y ( x R y -> y R x ) /\ A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) ) /\ Rel R ) )