Metamath Proof Explorer

Theorem elcoeleqvrelsrel

Description: For sets, being an element of the class of coelement equivalence relations is equivalent to satisfying the coelement equivalence relation predicate. (Contributed by Peter Mazsa, 24-Jul-2023)

Ref Expression
Assertion elcoeleqvrelsrel ⊢A∈V→A∈CoElEqvRels↔CoElEqvRelA

Proof

Step Hyp Ref Expression
1 elcoeleqvrels ⊢A∈V→A∈CoElEqvRels↔≀E-1↾A∈EqvRels
2 1cosscnvepresex ⊢A∈V→≀E-1↾A∈V
3 eleqvrelsrel ⊢≀E-1↾A∈V→≀E-1↾A∈EqvRels↔EqvRel≀E-1↾A
4 2 3 syl ⊢A∈V→≀E-1↾A∈EqvRels↔EqvRel≀E-1↾A
5 1 4 bitrd ⊢A∈V→A∈CoElEqvRels↔EqvRel≀E-1↾A
6 df-coeleqvrel ⊢CoElEqvRelA↔EqvRel≀E-1↾A
7 5 6 bitr4di ⊢A∈V→A∈CoElEqvRels↔CoElEqvRelA