Metamath Proof Explorer

Theorem dfcoeleqvrels

Description: Alternate definition of the coelement equivalence relations class. Other alternate definitions should be based on eqvrelcoss2 , eqvrelcoss3 and eqvrelcoss4 when needed. (Contributed by Peter Mazsa, 28-Nov-2022)

Ref Expression
Assertion dfcoeleqvrels ⊢ CoElEqvRels = a | ∼ a ∈ EqvRels

Proof

Step Hyp Ref Expression
1 df-coeleqvrels ⊢ CoElEqvRels = a | ≀ E -1 ↾ a ∈ EqvRels
2 df-coels ⊢ ∼ a = ≀ E -1 ↾ a
3 2 eleq1i ⊢ ∼ a ∈ EqvRels ↔ ≀ E -1 ↾ a ∈ EqvRels
4 3 abbii ⊢ a | ∼ a ∈ EqvRels = a | ≀ E -1 ↾ a ∈ EqvRels
5 1 4 eqtr4i ⊢ CoElEqvRels = a | ∼ a ∈ EqvRels