Metamath Proof Explorer

Theorem dfmember

Description: Alternate definition of the membership equivalence relation. (Contributed by Peter Mazsa, 28-Nov-2022)

Ref Expression
Assertion dfmember 
|- ( MembEr A <-> ~ A ErALTV A )

Proof

Step Hyp Ref Expression
1 df-member 
 |-  ( MembEr A <-> ,~ ( `' _E |` A ) ErALTV A )
2 df-coels 
 |-  ~ A = ,~ ( `' _E |` A )
3 2 erALTVeq1i 
 |-  ( ~ A ErALTV A <-> ,~ ( `' _E |` A ) ErALTV A )
4 1 3 bitr4i 
 |-  ( MembEr A <-> ~ A ErALTV A )