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

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