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 ∼ 𝐴 )