Theorem dfcoeleqvrel

Description: Alternate definition of the coelement equivalence relation predicate: a coelement equivalence relation is an equivalence relation on coelements. Other alternate definitions should be based on eqvrelcoss2 , eqvrelcoss3 and eqvrelcoss4 when needed. (Contributed by Peter Mazsa, 28-Nov-2022)

	Ref	Expression
Assertion	dfcoeleqvrel	|- ( CoElEqvRel A <-> EqvRel ~ A )

Proof

Step	Hyp	Ref	Expression
1		df-coeleqvrel	|- ( CoElEqvRel A <-> EqvRel ,~ ( `' _E |` A ) )
2		df-coels	|- ~ A = ,~ ( `' _E |` A )
3	2	eqvreleqi	|- ( EqvRel ~ A <-> EqvRel ,~ ( `' _E |` A ) )
4	1 3	bitr4i	|- ( CoElEqvRel A <-> EqvRel ~ A )