Metamath Proof Explorer


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 A EqvRel E -1 A

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA class A
1 0 wcoeleqvrel wff CoElEqvRel A
2 cep class E
3 2 ccnv class E -1
4 3 0 cres class E -1 A
5 4 ccoss class E -1 A
6 5 weqvrel wff EqvRel E -1 A
7 1 6 wb wff CoElEqvRel A EqvRel E -1 A