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	⊢ ( CoMembEr 𝐴 ↔ ≀ ( ◡ E ↾ 𝐴 ) ErALTV 𝐴 )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1	0	wcomember	⊢ CoMembEr 𝐴
2		cep	⊢ E
3	2	ccnv	⊢ ◡ E
4	3 0	cres	⊢ ( ◡ E ↾ 𝐴 )
5	4	ccoss	⊢ ≀ ( ◡ E ↾ 𝐴 )
6	0 5	werALTV	⊢ ≀ ( ◡ E ↾ 𝐴 ) ErALTV 𝐴
7	1 6	wb	⊢ ( CoMembEr 𝐴 ↔ ≀ ( ◡ E ↾ 𝐴 ) ErALTV 𝐴 )