Definition df-er 5910

Description: Define the set of all equivalence relationships over a base set. (Contributed by SF, 19-Feb-2015.)

Assertion

Ref	Expression
df-er	|- Er = ( Sym i^i Trans )

Detailed syntax breakdown of Definition df-er

Step	Hyp	Ref	Expression
1		cer 5899	. 2 class Er
2		csym 5898	. . 3 class Sym
3		ctrans 5889	. . 3 class Trans
4	2, 3	cin 3209	. 2 class ( Sym i^i Trans )
5	1, 4	wceq 1642	1 wff Er = ( Sym i^i Trans )

This definition is referenced by:  erex  5921  ersymtr  5933