Definition df-comember

Description: Define the comember equivalence relation on the class A (or, the restricted coelement equivalence relation on its domain quotient A .) Alternate definitions are dfcomember2 and dfcomember3 .

Later on, in an application of set theory I make a distinction between the default elementhood concept and a special membership concept: membership equivalence relation will be an integral part of that membership concept. (Contributed by Peter Mazsa, 26-Jun-2021) (Revised by Peter Mazsa, 28-Nov-2022)

	Ref	Expression
Assertion	df-comember	$$⊢CoMembErA\leftrightarrow \wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)ErALTVA$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1	0	wcomember	$$wffCoMembErA$$
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	0 5	werALTV	$$wff\wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)ErALTVA$$
7	1 6	wb	$$wff\left(CoMembErA\leftrightarrow \wr \left({{\mathrm{E}}^{-1}\upharpoonright }_A\right)ErALTVA\right)$$