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 A <-> ,~ ( `' _E |` A ) ErALTV A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cA | |- A |
|
| 1 | 0 | wmember | |- MembEr A |
| 2 | cep | |- _E |
|
| 3 | 2 | ccnv | |- `' _E |
| 4 | 3 0 | cres | |- ( `' _E |` A ) |
| 5 | 4 | ccoss | |- ,~ ( `' _E |` A ) |
| 6 | 0 5 | werALTV | |- ,~ ( `' _E |` A ) ErALTV A |
| 7 | 1 6 | wb | |- ( MembEr A <-> ,~ ( `' _E |` A ) ErALTV A ) |