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 -1 ↾ A ErALTV A
2 df-coels ⊢ ∼ A = ≀ E -1 ↾ A
3 2 erALTVeq1i ⊢ ∼ A ErALTV A ↔ ≀ E -1 ↾ A ErALTV A
4 1 3 bitr4i ⊢ MembEr A ↔ ∼ A ErALTV A