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	Could not format assertion : No typesetting found for |- ( CoMembEr A <-> ,~ ( `' _E |` A ) ErALTV A ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1	0	wcomember	Could not format CoMembEr A : No typesetting found for wff CoMembEr A with typecode wff
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	Could not format ( CoMembEr A <-> ,~ ( `' _E |` A ) ErALTV A ) : No typesetting found for wff ( CoMembEr A <-> ,~ ( `' _E |` A ) ErALTV A ) with typecode wff