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	$$⊢CoElEqvRelA\leftrightarrow EqvRel\sim A$$

Proof

Step	Hyp	Ref	Expression
1		df-coeleqvrel	$$⊢CoElEqvRelA\leftrightarrow EqvRel\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$
2		df-coels	$$⊢\sim A=\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$
3	2	eqvreleqi	$$⊢EqvRel\sim A\leftrightarrow EqvRel\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$
4	1 3	bitr4i	$$⊢CoElEqvRelA\leftrightarrow EqvRel\sim A$$