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

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 = { 𝑎 ∣ ∼ 𝑎 ∈ EqvRels }

Proof

Step Hyp Ref Expression
1 df-coeleqvrels ⊢ CoElEqvRels = { 𝑎 ∣ ≀ ( ◡ E ↾ 𝑎 ) ∈ EqvRels }
2 df-coels ⊢ ∼ 𝑎 = ≀ ( ◡ E ↾ 𝑎 )
3 2 eleq1i ⊢ ( ∼ 𝑎 ∈ EqvRels ↔ ≀ ( ◡ E ↾ 𝑎 ) ∈ EqvRels )
4 3 abbii ⊢ { 𝑎 ∣ ∼ 𝑎 ∈ EqvRels } = { 𝑎 ∣ ≀ ( ◡ E ↾ 𝑎 ) ∈ EqvRels }
5 1 4 eqtr4i ⊢ CoElEqvRels = { 𝑎 ∣ ∼ 𝑎 ∈ EqvRels }