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

Theorem sspwb 4239
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 3199 . . . . 5  |-  ( x 
C_  A  ->  ( A  C_  B  ->  x  C_  B ) )
21com12 27 . . . 4  |-  ( A 
C_  B  ->  (
x  C_  A  ->  x 
C_  B ) )
3 vex 2804 . . . . 5  |-  x  e. 
_V
43elpw 3644 . . . 4  |-  ( x  e.  ~P A  <->  x  C_  A
)
53elpw 3644 . . . 4  |-  ( x  e.  ~P B  <->  x  C_  B
)
62, 4, 53imtr4g 261 . . 3  |-  ( A 
C_  B  ->  (
x  e.  ~P A  ->  x  e.  ~P B
) )
76ssrdv 3198 . 2  |-  ( A 
C_  B  ->  ~P A  C_  ~P B )
8 ssel 3187 . . . 4  |-  ( ~P A  C_  ~P B  ->  ( { x }  e.  ~P A  ->  { x }  e.  ~P B
) )
9 snex 4232 . . . . . 6  |-  { x }  e.  _V
109elpw 3644 . . . . 5  |-  ( { x }  e.  ~P A 
<->  { x }  C_  A )
113snss 3761 . . . . 5  |-  ( x  e.  A  <->  { x }  C_  A )
1210, 11bitr4i 243 . . . 4  |-  ( { x }  e.  ~P A 
<->  x  e.  A )
139elpw 3644 . . . . 5  |-  ( { x }  e.  ~P B 
<->  { x }  C_  B )
143snss 3761 . . . . 5  |-  ( x  e.  B  <->  { x }  C_  B )
1513, 14bitr4i 243 . . . 4  |-  ( { x }  e.  ~P B 
<->  x  e.  B )
168, 12, 153imtr3g 260 . . 3  |-  ( ~P A  C_  ~P B  ->  ( x  e.  A  ->  x  e.  B ) )
1716ssrdv 3198 . 2  |-  ( ~P A  C_  ~P B  ->  A  C_  B )
187, 17impbii 180 1  |-  ( A 
C_  B  <->  ~P A  C_ 
~P B )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    e. wcel 1696    C_ wss 3165   ~Pcpw 3638   {csn 3653
This theorem is referenced by:  pwel  4241  ssextss  4243  pweqb  4246  pwdom  7029  marypha1lem  7202  wdompwdom  7308  r1pwss  7472  pwwf  7495  rankpwi  7511  rankxplim  7565  ackbij2lem1  7861  fictb  7887  ssfin2  7962  ssfin3ds  7972  ttukeylem2  8153  hashbclem  11406  wrdexg  11441  incexclem  12311  hashbcss  13067  isacs1i  13575  mreacs  13576  acsfn  13577  sscpwex  13708  wunfunc  13789  isacs3lem  14285  isacs5lem  14288  tgcmp  17144  imastopn  17427  fgabs  17590  fgtr  17601  trfg  17602  ssufl  17629  alexsubb  17756  tsmsres  17842  cfilresi  18737  cmetss  18756  minveclem4a  18810  minveclem4  18812  vitali  18984  sqff1o  20436  ballotlem2  23063  elsigagen2  23524  measres  23564  imambfm  23582  lemindclsbu  26098  neibastop1  26411  neibastop2lem  26412  neibastop2  26413  sstotbnd2  26601  isnacs3  26888  aomclem2  27255
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pr 4230
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-pw 3640  df-sn 3659  df-pr 3660
  Copyright terms: Public domain W3C validator