Theorem dfcomember3

Description: Alternate definition of the comember equivalence relation. (Contributed by Peter Mazsa, 26-Sep-2021) (Revised by Peter Mazsa, 17-Jul-2023)

	Ref	Expression
Assertion	dfcomember3	|- ( CoMembEr A <-> ( CoElEqvRel A /\ ( U. A /. ~ A ) = A ) )

Proof

Step	Hyp	Ref	Expression
1		dfcomember2	|- ( CoMembEr A <-> ( EqvRel ~ A /\ ( dom ~ A /. ~ A ) = A ) )
2		dfcoeleqvrel	|- ( CoElEqvRel A <-> EqvRel ~ A )
3	2	bicomi	|- ( EqvRel ~ A <-> CoElEqvRel A )
4		dmqscoelseq	|- ( ( dom ~ A /. ~ A ) = A <-> ( U. A /. ~ A ) = A )
5	3 4	anbi12i	|- ( ( EqvRel ~ A /\ ( dom ~ A /. ~ A ) = A ) <-> ( CoElEqvRel A /\ ( U. A /. ~ A ) = A ) )
6	1 5	bitri	|- ( CoMembEr A <-> ( CoElEqvRel A /\ ( U. A /. ~ A ) = A ) )