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

Metamath Proof Explorer

Theorem eldisjs

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

		Ref	Expression
	Assertion	eldisjs	$⊢ R \in Disjs \leftrightarrow (≀ R^{-1} \in CnvRefRels \land R \in Rels)$

Step	Hyp	Ref	Expression
1		dfdisjs	$⊢ Disjs = \{r \in Rels \| ≀ r^{-1} \in CnvRefRels\}$
2		cnveq	$⊢ r = R \to r^{-1} = R^{-1}$
3	2	cosseqd	$⊢ r = R \to ≀ r^{-1} = ≀ R^{-1}$
4	3	eleq1d	$⊢ r = R \to (≀ r^{-1} \in CnvRefRels \leftrightarrow ≀ R^{-1} \in CnvRefRels)$
5	1 4	rabeqel	$⊢ R \in Disjs \leftrightarrow (≀ R^{-1} \in CnvRefRels \land R \in Rels)$