Metamath Proof Explorer

Theorem dfcomember

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

Ref Expression
Assertion dfcomember ⊢ CoMembEr A ↔ ∼ A ErALTV A

Proof

Step Hyp Ref Expression
1 df-comember ⊢ CoMembEr 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 ⊢ CoMembEr A ↔ ∼ A ErALTV A