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 ↔ CoElEqvRel A

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 ⊢ CoElEqvRel A ↔ EqvRel ≀ E -1 ↾ A
7 5 6 bitr4di ⊢ A ∈ V → A ∈ CoElEqvRels ↔ CoElEqvRel A