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	$$⊢CoMembErA\leftrightarrow \left(CoElEqvRelA\wedge \bigcup A/\sim A=A\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfcomember2	$$⊢CoMembErA\leftrightarrow \left(EqvRel\sim A\wedge \mathrm{dom}\sim A/\sim A=A\right)$$
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	$$⊢CoMembErA\leftrightarrow \left(CoElEqvRelA\wedge \bigcup A/\sim A=A\right)$$