Metamath Proof Explorer

Theorem dfmember2

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

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

Proof

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