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

Metamath Proof Explorer

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