Metamath Proof Explorer

Theorem elcoeleqvrels

Description: Elementhood in the coelement equivalence relations class. (Contributed by Peter Mazsa, 24-Jul-2023)

Ref Expression
Assertion elcoeleqvrels ⊢ A ∈ V → A ∈ CoElEqvRels ↔ ≀ E -1 ↾ A ∈ EqvRels

Proof

Step Hyp Ref Expression
1 reseq2 ⊢ a = A → E -1 ↾ a = E -1 ↾ A
2 1 cosseqd ⊢ a = A → ≀ E -1 ↾ a = ≀ E -1 ↾ A
3 2 eleq1d ⊢ a = A → ≀ E -1 ↾ a ∈ EqvRels ↔ ≀ E -1 ↾ A ∈ EqvRels
4 df-coeleqvrels ⊢ CoElEqvRels = a | ≀ E -1 ↾ a ∈ EqvRels
5 3 4 elab2g ⊢ A ∈ V → A ∈ CoElEqvRels ↔ ≀ E -1 ↾ A ∈ EqvRels