Metamath Proof Explorer

Theorem cosselrels

Description: Cosets of sets are elements of the relations class. Implies |- ( R e. Rels -> ,R e. Rels ) . (Contributed by Peter Mazsa, 25-Aug-2021)

		Ref	Expression
	Assertion	cosselrels	$⊢ A \in V \to ≀ A \in Rels$

Proof

Step	Hyp	Ref	Expression
1		cossex	$⊢ A \in V \to ≀ A \in V$
2		relcoss	$⊢ Rel ≀ A$
3		elrelsrel	$⊢ ≀ A \in V \to (≀ A \in Rels \leftrightarrow Rel ≀ A)$
4	2 3	mpbiri	$⊢ ≀ A \in V \to ≀ A \in Rels$
5	1 4	syl	$⊢ A \in V \to ≀ A \in Rels$