Theorem dfcoeleqvrels

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

	Ref	Expression
Assertion	dfcoeleqvrels	$$⊢\mathrm{CoElEqvRels}=\left\{a|\sim a\in \mathrm{EqvRels}\right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-coeleqvrels	$$⊢\mathrm{CoElEqvRels}=\left\{a|\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)\in \mathrm{EqvRels}\right\}$$
2		df-coels	$$⊢\sim a=\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)$$
3	2	eleq1i	$$⊢\sim a\in \mathrm{EqvRels}\leftrightarrow \wr \left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)\in \mathrm{EqvRels}$$
4	3	abbii	$$⊢\left\{a|\sim a\in \mathrm{EqvRels}\right\}=\left\{a|\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_a\right)\in \mathrm{EqvRels}\right\}$$
5	1 4	eqtr4i	$$⊢\mathrm{CoElEqvRels}=\left\{a|\sim a\in \mathrm{EqvRels}\right\}$$