Definition df-coeleqvrel

Description: Define the coelement equivalence relation predicate. (Read: the coelement equivalence relation on A .) Alternate definition is dfcoeleqvrel . For sets, being an element of the class of coelement equivalence relations is equivalent to satisfying the coelement equivalence relation predicate, see elcoeleqvrelsrel . (Contributed by Peter Mazsa, 11-Dec-2021)

	Ref	Expression
Assertion	df-coeleqvrel	$$⊢CoElEqvRelA\leftrightarrow EqvRel\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1	0	wcoeleqvrel	$$wffCoElEqvRelA$$
2		cep	$$class\mathrm{E}$$
3	2	ccnv	$$class{\mathrm{E}}^{-1}$$
4	3 0	cres	$$class\left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$
5	4	ccoss	$$class\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$
6	5	weqvrel	$$wffEqvRel\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)$$
7	1 6	wb	$$wff\left(CoElEqvRelA\leftrightarrow EqvRel\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)\right)$$