Metamath Proof Explorer


Theorem eldisjs

Description: Elementhood in the class of disjoints. (Contributed by Peter Mazsa, 24-Jul-2021)

Ref Expression
Assertion eldisjs R Disjs R -1 CnvRefRels R Rels

Proof

Step Hyp Ref Expression
1 dfdisjs Disjs = r Rels | r -1 CnvRefRels
2 cnveq r = R r -1 = R -1
3 2 cosseqd r = R r -1 = R -1
4 3 eleq1d r = R r -1 CnvRefRels R -1 CnvRefRels
5 1 4 rabeqel R Disjs R -1 CnvRefRels R Rels