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 
|- ( A e. V -> ( A e. CoElEqvRels <-> CoElEqvRel A ) )

Proof

Step Hyp Ref Expression
1 elcoeleqvrels 
 |-  ( A e. V -> ( A e. CoElEqvRels <-> ,~ ( `' _E |` A ) e. EqvRels ) )
2 1cosscnvepresex 
 |-  ( A e. V -> ,~ ( `' _E |` A ) e. _V )
3 eleqvrelsrel 
 |-  ( ,~ ( `' _E |` A ) e. _V -> ( ,~ ( `' _E |` A ) e. EqvRels <-> EqvRel ,~ ( `' _E |` A ) ) )
4 2 3 syl 
 |-  ( A e. V -> ( ,~ ( `' _E |` A ) e. EqvRels <-> EqvRel ,~ ( `' _E |` A ) ) )
5 1 4 bitrd 
 |-  ( A e. V -> ( A e. CoElEqvRels <-> EqvRel ,~ ( `' _E |` A ) ) )
6 df-coeleqvrel 
 |-  ( CoElEqvRel A <-> EqvRel ,~ ( `' _E |` A ) )
7 5 6 bitr4di 
 |-  ( A e. V -> ( A e. CoElEqvRels <-> CoElEqvRel A ) )