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 |` A ) ErALTV A )
2 df-coels 
 |-  ~ A = ,~ ( `' _E |` A )
3 2 erALTVeq1i 
 |-  ( ~ A ErALTV A <-> ,~ ( `' _E |` A ) ErALTV A )
4 1 3 bitr4i 
 |-  ( CoMembEr A <-> ~ A ErALTV A )