Theorem dfmember3

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

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

Proof

Step	Hyp	Ref	Expression
1		dfmember2	|- ( MembEr 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	|- ( MembEr A <-> ( CoElEqvRel A /\ ( U. A /. ~ A ) = A ) )