Theorem elcoeleqvrelsrel

Description: For sets, being an element of the class of coelement equivalence relations is equivalent to satisfying the coelement equivalence relation predicate. (Contributed by Peter Mazsa, 24-Jul-2023)

	Ref	Expression
Assertion	elcoeleqvrelsrel	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ CoElEqvRels ↔ CoElEqvRel 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		elcoeleqvrels	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ CoElEqvRels ↔ ≀ ( ◡ E ↾ 𝐴 ) ∈ EqvRels ) )
2		1cosscnvepresex	⊢ ( 𝐴 ∈ 𝑉 → ≀ ( ◡ E ↾ 𝐴 ) ∈ V )
3		eleqvrelsrel	⊢ ( ≀ ( ◡ E ↾ 𝐴 ) ∈ V → ( ≀ ( ◡ E ↾ 𝐴 ) ∈ EqvRels ↔ EqvRel ≀ ( ◡ E ↾ 𝐴 ) ) )
4	2 3	syl	⊢ ( 𝐴 ∈ 𝑉 → ( ≀ ( ◡ E ↾ 𝐴 ) ∈ EqvRels ↔ EqvRel ≀ ( ◡ E ↾ 𝐴 ) ) )
5	1 4	bitrd	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ CoElEqvRels ↔ EqvRel ≀ ( ◡ E ↾ 𝐴 ) ) )
6		df-coeleqvrel	⊢ ( CoElEqvRel 𝐴 ↔ EqvRel ≀ ( ◡ E ↾ 𝐴 ) )
7	5 6	bitr4di	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ CoElEqvRels ↔ CoElEqvRel 𝐴 ) )