Theorem dfcomember2

Description: Alternate definition of the comember equivalence relation. (Contributed by Peter Mazsa, 25-Sep-2021)

	Ref	Expression
Assertion	dfcomember2	⊢ ( CoMembEr 𝐴 ↔ ( EqvRel ∼ 𝐴 ∧ ( dom ∼ 𝐴 / ∼ 𝐴 ) = 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		dfcomember	⊢ ( CoMembEr 𝐴 ↔ ∼ 𝐴 ErALTV 𝐴 )
2		dferALTV2	⊢ ( ∼ 𝐴 ErALTV 𝐴 ↔ ( EqvRel ∼ 𝐴 ∧ ( dom ∼ 𝐴 / ∼ 𝐴 ) = 𝐴 ) )
3	1 2	bitri	⊢ ( CoMembEr 𝐴 ↔ ( EqvRel ∼ 𝐴 ∧ ( dom ∼ 𝐴 / ∼ 𝐴 ) = 𝐴 ) )