MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  qsss Unicode version

Theorem qsss 6762
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.)
Hypothesis
Ref Expression
qsss.1  |-  ( ph  ->  R  Er  A )
Assertion
Ref Expression
qsss  |-  ( ph  ->  ( A /. R
)  C_  ~P A
)

Proof of Theorem qsss
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 vex 2825 . . . 4  |-  x  e. 
_V
21elqs 6754 . . 3  |-  ( x  e.  ( A /. R )  <->  E. y  e.  A  x  =  [ y ] R
)
3 qsss.1 . . . . . . 7  |-  ( ph  ->  R  Er  A )
43ecss 6743 . . . . . 6  |-  ( ph  ->  [ y ] R  C_  A )
5 sseq1 3233 . . . . . 6  |-  ( x  =  [ y ] R  ->  ( x  C_  A  <->  [ y ] R  C_  A ) )
64, 5syl5ibrcom 213 . . . . 5  |-  ( ph  ->  ( x  =  [
y ] R  ->  x  C_  A ) )
71elpw 3665 . . . . 5  |-  ( x  e.  ~P A  <->  x  C_  A
)
86, 7syl6ibr 218 . . . 4  |-  ( ph  ->  ( x  =  [
y ] R  ->  x  e.  ~P A
) )
98rexlimdvw 2704 . . 3  |-  ( ph  ->  ( E. y  e.  A  x  =  [
y ] R  ->  x  e.  ~P A
) )
102, 9syl5bi 208 . 2  |-  ( ph  ->  ( x  e.  ( A /. R )  ->  x  e.  ~P A ) )
1110ssrdv 3219 1  |-  ( ph  ->  ( A /. R
)  C_  ~P A
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1633    e. wcel 1701   E.wrex 2578    C_ wss 3186   ~Pcpw 3659    Er wer 6699   [cec 6700   /.cqs 6701
This theorem is referenced by:  axcnex  8814  wuncn  8837  qshash  12332  lagsubg2  14727  lagsubg  14728  orbsta2  14817  sylow1lem3  14960  sylow2alem2  14978  sylow2a  14979  sylow2blem2  14981  sylow2blem3  14982  sylow3lem3  14989  sylow3lem4  14990  vitalilem5  19020  vitali  19021
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-14 1705  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297  ax-sep 4178  ax-nul 4186  ax-pr 4251
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-eu 2180  df-mo 2181  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-ne 2481  df-ral 2582  df-rex 2583  df-rab 2586  df-v 2824  df-dif 3189  df-un 3191  df-in 3193  df-ss 3200  df-nul 3490  df-if 3600  df-pw 3661  df-sn 3680  df-pr 3681  df-op 3683  df-br 4061  df-opab 4115  df-xp 4732  df-rel 4733  df-cnv 4734  df-dm 4736  df-rn 4737  df-res 4738  df-ima 4739  df-er 6702  df-ec 6704  df-qs 6708
  Copyright terms: Public domain W3C validator