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

Theorem qsss 6966
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 2960 . . . 4  |-  x  e. 
_V
21elqs 6958 . . 3  |-  ( x  e.  ( A /. R )  <->  E. y  e.  A  x  =  [ y ] R
)
3 qsss.1 . . . . . . 7  |-  ( ph  ->  R  Er  A )
43ecss 6947 . . . . . 6  |-  ( ph  ->  [ y ] R  C_  A )
5 sseq1 3370 . . . . . 6  |-  ( x  =  [ y ] R  ->  ( x  C_  A  <->  [ y ] R  C_  A ) )
64, 5syl5ibrcom 215 . . . . 5  |-  ( ph  ->  ( x  =  [
y ] R  ->  x  C_  A ) )
71elpw 3806 . . . . 5  |-  ( x  e.  ~P A  <->  x  C_  A
)
86, 7syl6ibr 220 . . . 4  |-  ( ph  ->  ( x  =  [
y ] R  ->  x  e.  ~P A
) )
98rexlimdvw 2834 . . 3  |-  ( ph  ->  ( E. y  e.  A  x  =  [
y ] R  ->  x  e.  ~P A
) )
102, 9syl5bi 210 . 2  |-  ( ph  ->  ( x  e.  ( A /. R )  ->  x  e.  ~P A ) )
1110ssrdv 3355 1  |-  ( ph  ->  ( A /. R
)  C_  ~P A
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    e. wcel 1726   E.wrex 2707    C_ wss 3321   ~Pcpw 3800    Er wer 6903   [cec 6904   /.cqs 6905
This theorem is referenced by:  axcnex  9023  wuncn  9046  qshash  12607  lagsubg2  15002  lagsubg  15003  orbsta2  15092  sylow1lem3  15235  sylow2alem2  15253  sylow2a  15254  sylow2blem2  15256  sylow2blem3  15257  sylow3lem3  15264  sylow3lem4  15265  vitalilem5  19505  vitali  19506
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418  ax-sep 4331  ax-nul 4339  ax-pr 4404
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2286  df-mo 2287  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-ral 2711  df-rex 2712  df-rab 2715  df-v 2959  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3630  df-if 3741  df-pw 3802  df-sn 3821  df-pr 3822  df-op 3824  df-br 4214  df-opab 4268  df-xp 4885  df-rel 4886  df-cnv 4887  df-dm 4889  df-rn 4890  df-res 4891  df-ima 4892  df-er 6906  df-ec 6908  df-qs 6912
  Copyright terms: Public domain W3C validator