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

Metamath Proof Explorer

Theorem cossex

Description: If A is a set then the class of cosets by A is a set. (Contributed by Peter Mazsa, 4-Jan-2019)

		Ref	Expression
	Assertion	cossex	$⊢ A \in V \to ≀ A \in V$

Step	Hyp	Ref	Expression
1		dfcoss3	$⊢ ≀ A = A \circ A^{-1}$
2		cnvexg	$⊢ A \in V \to A^{-1} \in V$
3		coexg	$⊢ (A \in V \land A^{-1} \in V) \to A \circ A^{-1} \in V$
4	2 3	mpdan	$⊢ A \in V \to A \circ A^{-1} \in V$
5	1 4	eqeltrid	$⊢ A \in V \to ≀ A \in V$