Theorem eldisjsdisj

Description: The element of the class of disjoint relations and the disjoint relation predicate are the same, that is ( R e. Disjs <-> Disj R ) when R is a set. (Contributed by Peter Mazsa, 25-Jul-2021)

	Ref	Expression
Assertion	eldisjsdisj	|- ( R e. V -> ( R e. Disjs <-> Disj R ) )

Proof

Step	Hyp	Ref	Expression
1		cosscnvex	|- ( R e. V -> ,~ `' R e. _V )
2		elcnvrefrelsrel	|- ( ,~ `' R e. _V -> ( ,~ `' R e. CnvRefRels <-> CnvRefRel ,~ `' R ) )
3	1 2	syl	|- ( R e. V -> ( ,~ `' R e. CnvRefRels <-> CnvRefRel ,~ `' R ) )
4		elrelsrel	|- ( R e. V -> ( R e. Rels <-> Rel R ) )
5	3 4	anbi12d	|- ( R e. V -> ( ( ,~ `' R e. CnvRefRels /\ R e. Rels ) <-> ( CnvRefRel ,~ `' R /\ Rel R ) ) )
6		eldisjs	|- ( R e. Disjs <-> ( ,~ `' R e. CnvRefRels /\ R e. Rels ) )
7		df-disjALTV	|- ( Disj R <-> ( CnvRefRel ,~ `' R /\ Rel R ) )
8	5 6 7	3bitr4g	|- ( R e. V -> ( R e. Disjs <-> Disj R ) )