Definition df-comember 37531

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

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.)

Assertion

Ref	Expression
df-comember	⊢ ( CoMembEr 𝐴 ↔ ≀ (◡ E ↾ 𝐴) ErALTV 𝐴)

Detailed syntax breakdown of Definition df-comember

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	wcomember 37066	. 2 wff CoMembEr 𝐴
3		cep 5579	. . . . . 6 class E
4	3	ccnv 5675	. . . . 5 class ◡ E
5	4, 1	cres 5678	. . . 4 class (◡ E ↾ 𝐴)
6	5	ccoss 37038	. . 3 class ≀ (◡ E ↾ 𝐴)
7	1, 6	werALTV 37064	. 2 wff ≀ (◡ E ↾ 𝐴) ErALTV 𝐴
8	2, 7	wb 205	1 wff ( CoMembEr 𝐴 ↔ ≀ (◡ E ↾ 𝐴) ErALTV 𝐴)

This definition is referenced by:  dfcomember  37537  mpet2  37705