Metamath Proof Explorer

Theorem dfcomember2

Description: Alternate definition of the comember equivalence relation. (Contributed by Peter Mazsa, 25-Sep-2021)

Ref Expression
Assertion dfcomember2 
|- ( CoMembEr A <-> ( EqvRel ~ A /\ ( dom ~ A /. ~ A ) = A ) )

Proof

Step Hyp Ref Expression
1 dfcomember 
 |-  ( CoMembEr A <-> ~ A ErALTV A )
2 dferALTV2 
 |-  ( ~ A ErALTV A <-> ( EqvRel ~ A /\ ( dom ~ A /. ~ A ) = A ) )
3 1 2 bitri 
 |-  ( CoMembEr A <-> ( EqvRel ~ A /\ ( dom ~ A /. ~ A ) = A ) )