This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfcomember2

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

Ref Expression
Assertion dfcomember2 ⊢ CoMembEr A ↔ EqvRel ∼ A ∧ dom ⁡ ∼ A / ∼ A = A

Proof

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