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 ) )