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

Theorem sspwb 4354
Description: Classes are subclasses if and only if their power classes are subclasses. Exercise 18 of [TakeutiZaring] p. 18. (Contributed by NM, 13-Oct-1996.)
Assertion
Ref Expression
sspwb  |-  ( A 
C_  B  <->  ~P A  C_ 
~P B )

Proof of Theorem sspwb
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 sstr2 3298 . . . . 5  |-  ( x 
C_  A  ->  ( A  C_  B  ->  x  C_  B ) )
21com12 29 . . . 4  |-  ( A 
C_  B  ->  (
x  C_  A  ->  x 
C_  B ) )
3 vex 2902 . . . . 5  |-  x  e. 
_V
43elpw 3748 . . . 4  |-  ( x  e.  ~P A  <->  x  C_  A
)
53elpw 3748 . . . 4  |-  ( x  e.  ~P B  <->  x  C_  B
)
62, 4, 53imtr4g 262 . . 3  |-  ( A 
C_  B  ->  (
x  e.  ~P A  ->  x  e.  ~P B
) )
76ssrdv 3297 . 2  |-  ( A 
C_  B  ->  ~P A  C_  ~P B )
8 ssel 3285 . . . 4  |-  ( ~P A  C_  ~P B  ->  ( { x }  e.  ~P A  ->  { x }  e.  ~P B
) )
9 snex 4346 . . . . . 6  |-  { x }  e.  _V
109elpw 3748 . . . . 5  |-  ( { x }  e.  ~P A 
<->  { x }  C_  A )
113snss 3869 . . . . 5  |-  ( x  e.  A  <->  { x }  C_  A )
1210, 11bitr4i 244 . . . 4  |-  ( { x }  e.  ~P A 
<->  x  e.  A )
139elpw 3748 . . . . 5  |-  ( { x }  e.  ~P B 
<->  { x }  C_  B )
143snss 3869 . . . . 5  |-  ( x  e.  B  <->  { x }  C_  B )
1513, 14bitr4i 244 . . . 4  |-  ( { x }  e.  ~P B 
<->  x  e.  B )
168, 12, 153imtr3g 261 . . 3  |-  ( ~P A  C_  ~P B  ->  ( x  e.  A  ->  x  e.  B ) )
1716ssrdv 3297 . 2  |-  ( ~P A  C_  ~P B  ->  A  C_  B )
187, 17impbii 181 1  |-  ( A 
C_  B  <->  ~P A  C_ 
~P B )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    e. wcel 1717    C_ wss 3263   ~Pcpw 3742   {csn 3757
This theorem is referenced by:  pwel  4356  ssextss  4358  pweqb  4361  pwdom  7195  marypha1lem  7373  wdompwdom  7479  r1pwss  7643  pwwf  7666  rankpwi  7682  rankxplim  7736  ackbij2lem1  8032  fictb  8058  ssfin2  8133  ssfin3ds  8143  ttukeylem2  8323  hashbclem  11628  wrdexg  11666  incexclem  12543  hashbcss  13299  isacs1i  13809  mreacs  13810  acsfn  13811  sscpwex  13942  wunfunc  14023  isacs3lem  14519  isacs5lem  14522  tgcmp  17386  imastopn  17673  fgabs  17832  fgtr  17843  trfg  17844  ssufl  17871  alexsubb  17998  tsmsres  18094  cfiluweak  18246  cfilresi  19119  cmetss  19138  minveclem4a  19198  minveclem4  19200  vitali  19372  sqff1o  20832  elsigagen2  24327  measres  24370  imambfm  24406  ballotlem2  24525  neibastop1  26079  neibastop2lem  26080  neibastop2  26081  sstotbnd2  26174  isnacs3  26455  aomclem2  26821
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271  ax-nul 4279  ax-pr 4344
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-v 2901  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-pw 3744  df-sn 3763  df-pr 3764
  Copyright terms: Public domain W3C validator