Metamath Proof Explorer

Theorem eltrrels3

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

Ref Expression
Assertion eltrrels3 
|- ( R e. TrRels <-> ( A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) /\ R e. Rels ) )

Proof

Step Hyp Ref Expression
1 dftrrels3 
 |-  TrRels = { r e. Rels | A. x A. y A. z ( ( x r y /\ y r z ) -> x r z ) }
2 breq 
 |-  ( r = R -> ( x r y <-> x R y ) )
3 breq 
 |-  ( r = R -> ( y r z <-> y R z ) )
4 2 3 anbi12d 
 |-  ( r = R -> ( ( x r y /\ y r z ) <-> ( x R y /\ y R z ) ) )
5 breq 
 |-  ( r = R -> ( x r z <-> x R z ) )
6 4 5 imbi12d 
 |-  ( r = R -> ( ( ( x r y /\ y r z ) -> x r z ) <-> ( ( x R y /\ y R z ) -> x R z ) ) )
7 6 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 ) ) )
8 7 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 ) ) )
9 1 8 rabeqel 
 |-  ( R e. TrRels <-> ( A. x A. y A. z ( ( x R y /\ y R z ) -> x R z ) /\ R e. Rels ) )