This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐴 ↔ 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 ↾ 𝐴 ) )