Metamath Proof Explorer


Theorem elcoeleqvrels

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

Ref Expression
Assertion elcoeleqvrels ( 𝐴𝑉 → ( 𝐴 ∈ CoElEqvRels ↔ ≀ ( E ↾ 𝐴 ) ∈ EqvRels ) )

Proof

Step Hyp Ref Expression
1 reseq2 ( 𝑎 = 𝐴 → ( E ↾ 𝑎 ) = ( E ↾ 𝐴 ) )
2 1 cosseqd ( 𝑎 = 𝐴 → ≀ ( E ↾ 𝑎 ) = ≀ ( E ↾ 𝐴 ) )
3 2 eleq1d ( 𝑎 = 𝐴 → ( ≀ ( E ↾ 𝑎 ) ∈ EqvRels ↔ ≀ ( E ↾ 𝐴 ) ∈ EqvRels ) )
4 df-coeleqvrels CoElEqvRels = { 𝑎 ∣ ≀ ( E ↾ 𝑎 ) ∈ EqvRels }
5 3 4 elab2g ( 𝐴𝑉 → ( 𝐴 ∈ CoElEqvRels ↔ ≀ ( E ↾ 𝐴 ) ∈ EqvRels ) )