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 e. V -> ,~ A e. Rels )

Proof

Step	Hyp	Ref	Expression
1		cossex	|- ( A e. V -> ,~ A e. _V )
2		relcoss	|- Rel ,~ A
3		elrelsrel	|- ( ,~ A e. _V -> ( ,~ A e. Rels <-> Rel ,~ A ) )
4	2 3	mpbiri	|- ( ,~ A e. _V -> ,~ A e. Rels )
5	1 4	syl	|- ( A e. V -> ,~ A e. Rels )