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 }