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 \leftrightarrow (CoElEqvRel A \land ⋃ A / \sim A = A)$

Proof

Step	Hyp	Ref	Expression
1		dfcomember2	$⊢ CoMembEr A \leftrightarrow (EqvRel \sim A \land dom \sim A / \sim A = A)$
2		dfcoeleqvrel	$⊢ CoElEqvRel A \leftrightarrow EqvRel \sim A$
3	2	bicomi	$⊢ EqvRel \sim A \leftrightarrow CoElEqvRel A$
4		dmqscoelseq	$⊢ dom \sim A / \sim A = A \leftrightarrow ⋃ A / \sim A = A$
5	3 4	anbi12i	$⊢ (EqvRel \sim A \land dom \sim A / \sim A = A) \leftrightarrow (CoElEqvRel A \land ⋃ A / \sim A = A)$
6	1 5	bitri	$⊢ CoMembEr A \leftrightarrow (CoElEqvRel A \land ⋃ A / \sim A = A)$

Metamath Proof Explorer

Theorem dfcomember3

Proof