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	$$⊢\phi \to R\mathrm{Er}A$$
Assertion	qsss	$$⊢\phi \to A/R\subseteq 𝒫A$$

Proof

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