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	|- ( ph -> R Er A )
Assertion	qsss	|- ( ph -> ( A /. R ) C_ ~P A )

Proof

Step	Hyp	Ref	Expression
1		qsss.1	|- ( ph -> R Er A )
2		vex	|- x e. _V
3	2	elqs	|- ( x e. ( A /. R ) <-> E. y e. A x = [ y ] R )
4	1	ecss	|- ( ph -> [ y ] R C_ A )
5		sseq1	|- ( x = [ y ] R -> ( x C_ A <-> [ y ] R C_ A ) )
6	4 5	syl5ibrcom	|- ( ph -> ( x = [ y ] R -> x C_ A ) )
7		velpw	|- ( x e. ~P A <-> x C_ A )
8	6 7	syl6ibr	|- ( ph -> ( x = [ y ] R -> x e. ~P A ) )
9	8	rexlimdvw	|- ( ph -> ( E. y e. A x = [ y ] R -> x e. ~P A ) )
10	3 9	syl5bi	|- ( ph -> ( x e. ( A /. R ) -> x e. ~P A ) )
11	10	ssrdv	|- ( ph -> ( A /. R ) C_ ~P A )