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

Metamath Proof Explorer

Theorem qsss

Description: A quotient set is a set of subsets of the base set. (Contributed by Mario Carneiro, 9-Jul-2014) (Revised by Mario Carneiro, 12-Aug-2015)

		Ref	Expression
	Hypothesis	qsss.1	$⊢ φ \to R Er A$
	Assertion	qsss	$⊢ φ \to A / R \subseteq 𝒫 A$

Proof

Step	Hyp	Ref	Expression
1		qsss.1	$⊢ φ \to R Er A$
2		vex	$⊢ x \in V$
3	2	elqs	$⊢ x \in (A / R) \leftrightarrow \exists y \in A x = [y] R$
4	1	ecss	$⊢ φ \to [y] R \subseteq A$
5		sseq1	$⊢ x = [y] R \to (x \subseteq A \leftrightarrow [y] R \subseteq A)$
6	4 5	syl5ibrcom	$⊢ φ \to (x = [y] R \to x \subseteq A)$
7		velpw	$⊢ x \in 𝒫 A \leftrightarrow x \subseteq A$
8	6 7	imbitrrdi	$⊢ φ \to (x = [y] R \to x \in 𝒫 A)$
9	8	rexlimdvw	$⊢ φ \to (\exists y \in A x = [y] R \to x \in 𝒫 A)$
10	3 9	biimtrid	$⊢ φ \to (x \in (A / R) \to x \in 𝒫 A)$
11	10	ssrdv	$⊢ φ \to A / R \subseteq 𝒫 A$