Definition df-coeleqvrel

Description: Define the coelement equivalence relation predicate. (Read: the coelement equivalence relation on A .) Alternate definition is dfcoeleqvrel . For sets, being an element of the class of coelement equivalence relations is equivalent to satisfying the coelement equivalence relation predicate, see elcoeleqvrelsrel . (Contributed by Peter Mazsa, 11-Dec-2021)

	Ref	Expression
Assertion	df-coeleqvrel	⊢ ( CoElEqvRel 𝐴 ↔ EqvRel ≀ ( ◡ E ↾ 𝐴 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1	0	wcoeleqvrel	⊢ CoElEqvRel 𝐴
2		cep	⊢ E
3	2	ccnv	⊢ ◡ E
4	3 0	cres	⊢ ( ◡ E ↾ 𝐴 )
5	4	ccoss	⊢ ≀ ( ◡ E ↾ 𝐴 )
6	5	weqvrel	⊢ EqvRel ≀ ( ◡ E ↾ 𝐴 )
7	1 6	wb	⊢ ( CoElEqvRel 𝐴 ↔ EqvRel ≀ ( ◡ E ↾ 𝐴 ) )