Metamath Proof Explorer

Theorem eleqvrels3

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

Ref Expression
Assertion eleqvrels3 
|- ( R e. EqvRels <-> ( ( 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 ) ) /\ R e. Rels ) )

Proof

Step Hyp Ref Expression
1 dfeqvrels3 
 |-  EqvRels = { r e. Rels | ( 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 ) ) }
2 dmeq 
 |-  ( r = R -> dom r = dom R )
3 breq 
 |-  ( r = R -> ( x r x <-> x R x ) )
4 2 3 raleqbidv 
 |-  ( r = R -> ( A. x e. dom r x r x <-> A. x e. dom R x R x ) )
5 breq 
 |-  ( r = R -> ( x r y <-> x R y ) )
6 breq 
 |-  ( r = R -> ( y r x <-> y R x ) )
7 5 6 imbi12d 
 |-  ( r = R -> ( ( x r y -> y r x ) <-> ( x R y -> y R x ) ) )
8 7 2albidv 
 |-  ( r = R -> ( A. x A. y ( x r y -> y r x ) <-> A. x A. y ( x R y -> y R x ) ) )
9 breq 
 |-  ( r = R -> ( y r z <-> y R z ) )
10 5 9 anbi12d 
 |-  ( r = R -> ( ( x r y /\ y r z ) <-> ( x R y /\ y R z ) ) )
11 breq 
 |-  ( r = R -> ( x r z <-> x R z ) )
12 10 11 imbi12d 
 |-  ( r = R -> ( ( ( x r y /\ y r z ) -> x r z ) <-> ( ( x R y /\ y R z ) -> x R z ) ) )
13 12 2albidv 
 |-  ( r = R -> ( A. y A. z ( ( x r y /\ y r z ) -> x r z ) <-> A. y A. z ( ( x R y /\ y R z ) -> x R z ) ) )
14 13 albidv 
 |-  ( r = R -> ( A. x A. y A. z ( ( x r y /\ y r z ) -> x r z ) <-> A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) ) )
15 4 8 14 3anbi123d 
 |-  ( r = 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 ) ) <-> ( 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 ) ) ) )
16 1 15 rabeqel 
 |-  ( R e. EqvRels <-> ( ( 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 ) ) /\ R e. Rels ) )