Theorem eqvrelcoss

Description: Two ways to express equivalent cosets. (Contributed by Peter Mazsa, 4-Jul-2020) (Revised by Peter Mazsa, 20-Dec-2021)

	Ref	Expression
Assertion	eqvrelcoss	$$⊢EqvRel\wr R\leftrightarrow TrRel\wr R$$

Proof

Step	Hyp	Ref	Expression
1		df-eqvrel	$$⊢EqvRel\wr R\leftrightarrow \left(RefRel\wr R\wedge SymRel\wr R\wedge TrRel\wr R\right)$$
2		refrelcoss	$$⊢RefRel\wr R$$
3		symrelcoss	$$⊢SymRel\wr R$$
4	2 3	triantru3	$$⊢TrRel\wr R\leftrightarrow \left(RefRel\wr R\wedge SymRel\wr R\wedge TrRel\wr R\right)$$
5	1 4	bitr4i	$$⊢EqvRel\wr R\leftrightarrow TrRel\wr R$$