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

Metamath Proof Explorer

Theorem dfcoeleqvrel

Description: Alternate definition of the coelement equivalence relation predicate: a coelement equivalence relation is an equivalence relation on coelements. Other alternate definitions should be based on eqvrelcoss2 , eqvrelcoss3 and eqvrelcoss4 when needed. (Contributed by Peter Mazsa, 28-Nov-2022)

Ref Expression
Assertion dfcoeleqvrel ( CoElEqvRel 𝐴 ↔ EqvRel ∼ 𝐴 )

Proof

Step Hyp Ref Expression
1 df-coeleqvrel ⊢ ( CoElEqvRel 𝐴 ↔ EqvRel ≀ ( ◡ E ↾ 𝐴 ) )
2 df-coels ⊢ ∼ 𝐴 = ≀ ( ◡ E ↾ 𝐴 )
3 2 eqvreleqi ⊢ ( EqvRel ∼ 𝐴 ↔ EqvRel ≀ ( ◡ E ↾ 𝐴 ) )
4 1 3 bitr4i ⊢ ( CoElEqvRel 𝐴 ↔ EqvRel ∼ 𝐴 )