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

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