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 
|- ( 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 imbitrrdi 
 |-  ( 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 biimtrid 
 |-  ( ph -> ( x e. ( A /. R ) -> x e. ~P A ) )
11 10 ssrdv 
 |-  ( ph -> ( A /. R ) C_ ~P A )