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	⊢ ( 𝐴 ∈ 𝑉 → ≀ 𝐴 ∈ Rels )

Proof

Step	Hyp	Ref	Expression
1		cossex	⊢ ( 𝐴 ∈ 𝑉 → ≀ 𝐴 ∈ V )
2		relcoss	⊢ Rel ≀ 𝐴
3		elrelsrel	⊢ ( ≀ 𝐴 ∈ V → ( ≀ 𝐴 ∈ Rels ↔ Rel ≀ 𝐴 ) )
4	2 3	mpbiri	⊢ ( ≀ 𝐴 ∈ V → ≀ 𝐴 ∈ Rels )
5	1 4	syl	⊢ ( 𝐴 ∈ 𝑉 → ≀ 𝐴 ∈ Rels )