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