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 𝐴 ↔ ( CoElEqvRel 𝐴 ∧ ( ∪ 𝐴 / ∼ 𝐴 ) = 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		dfcomember2	⊢ ( CoMembEr 𝐴 ↔ ( EqvRel ∼ 𝐴 ∧ ( dom ∼ 𝐴 / ∼ 𝐴 ) = 𝐴 ) )
2		dfcoeleqvrel	⊢ ( CoElEqvRel 𝐴 ↔ EqvRel ∼ 𝐴 )
3	2	bicomi	⊢ ( EqvRel ∼ 𝐴 ↔ CoElEqvRel 𝐴 )
4		dmqscoelseq	⊢ ( ( dom ∼ 𝐴 / ∼ 𝐴 ) = 𝐴 ↔ ( ∪ 𝐴 / ∼ 𝐴 ) = 𝐴 )
5	3 4	anbi12i	⊢ ( ( EqvRel ∼ 𝐴 ∧ ( dom ∼ 𝐴 / ∼ 𝐴 ) = 𝐴 ) ↔ ( CoElEqvRel 𝐴 ∧ ( ∪ 𝐴 / ∼ 𝐴 ) = 𝐴 ) )
6	1 5	bitri	⊢ ( CoMembEr 𝐴 ↔ ( CoElEqvRel 𝐴 ∧ ( ∪ 𝐴 / ∼ 𝐴 ) = 𝐴 ) )