Metamath Proof Explorer


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