Definition df-member

Description: Define the membership equivalence relation on the class A (or, the restricted elementhood equivalence relation on its domain quotient A .) Alternate definitions are dfmember2 and dfmember3 .

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1	0	wmember	⊢ MembEr 𝐴
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	⊢ ( MembEr 𝐴 ↔ ≀ ( ◡ E ↾ 𝐴 ) ErALTV 𝐴 )