Metamath Proof Explorer


Theorem eltrrelsrel

Description: For sets, being an element of the class of transitive relations is equivalent to satisfying the transitive relation predicate. (Contributed by Peter Mazsa, 22-Aug-2021)

Ref Expression
Assertion eltrrelsrel R V R TrRels TrRel R

Proof

Step Hyp Ref Expression
1 elrelsrel R V R Rels Rel R
2 1 anbi2d R V R R R R Rels R R R Rel R
3 eltrrels2 R TrRels R R R R Rels
4 dftrrel2 TrRel R R R R Rel R
5 2 3 4 3bitr4g R V R TrRels TrRel R