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	Could not format assertion : No typesetting found for |- ( CoMembEr A <-> ( CoElEqvRel A /\ ( U. A /. ~ A ) = A ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		dfcomember2	Could not format ( CoMembEr A <-> ( EqvRel ~ A /\ ( dom ~ A /. ~ A ) = A ) ) : No typesetting found for |- ( CoMembEr A <-> ( EqvRel ~ A /\ ( dom ~ A /. ~ A ) = A ) ) with typecode |-
2		dfcoeleqvrel	$$⊢CoElEqvRelA\leftrightarrow EqvRel\sim A$$
3	2	bicomi	$$⊢EqvRel\sim A\leftrightarrow CoElEqvRelA$$
4		dmqscoelseq	$$⊢\mathrm{dom}\sim A/\sim A=A\leftrightarrow \bigcup A/\sim A=A$$
5	3 4	anbi12i	$$⊢\left(EqvRel\sim A\wedge \mathrm{dom}\sim A/\sim A=A\right)\leftrightarrow \left(CoElEqvRelA\wedge \bigcup A/\sim A=A\right)$$
6	1 5	bitri	Could not format ( CoMembEr A <-> ( CoElEqvRel A /\ ( U. A /. ~ A ) = A ) ) : No typesetting found for |- ( CoMembEr A <-> ( CoElEqvRel A /\ ( U. A /. ~ A ) = A ) ) with typecode |-