Theorem relcoels

Description: Coelements on A is a relation. (Contributed by Peter Mazsa, 5-Oct-2021)

	Ref	Expression
Assertion	relcoels	⊢ Rel ∼ 𝐴

Proof

Step	Hyp	Ref	Expression
1		relcoss	⊢ Rel ≀ ( ◡ E ↾ 𝐴 )
2		df-coels	⊢ ∼ 𝐴 = ≀ ( ◡ E ↾ 𝐴 )
3	2	releqi	⊢ ( Rel ∼ 𝐴 ↔ Rel ≀ ( ◡ E ↾ 𝐴 ) )
4	1 3	mpbir	⊢ Rel ∼ 𝐴