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

Theorem sspwb 4222
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
StepHypRef Expression
1 sstr2 3187 . . . . 5  |-  ( x 
C_  A  ->  ( A  C_  B  ->  x  C_  B ) )
21com12 29 . . . 4  |-  ( A 
C_  B  ->  (
x  C_  A  ->  x 
C_  B ) )
3 vex 2792 . . . . 5  |-  x  e. 
_V
43elpw 3632 . . . 4  |-  ( x  e.  ~P A  <->  x  C_  A
)
53elpw 3632 . . . 4  |-  ( x  e.  ~P B  <->  x  C_  B
)
62, 4, 53imtr4g 263 . . 3  |-  ( A 
C_  B  ->  (
x  e.  ~P A  ->  x  e.  ~P B
) )
76ssrdv 3186 . 2  |-  ( A 
C_  B  ->  ~P A  C_  ~P B )
8 ssel 3175 . . . 4  |-  ( ~P A  C_  ~P B  ->  ( { x }  e.  ~P A  ->  { x }  e.  ~P B
) )
9 snex 4215 . . . . . 6  |-  { x }  e.  _V
109elpw 3632 . . . . 5  |-  ( { x }  e.  ~P A 
<->  { x }  C_  A )
113snss 3749 . . . . 5  |-  ( x  e.  A  <->  { x }  C_  A )
1210, 11bitr4i 245 . . . 4  |-  ( { x }  e.  ~P A 
<->  x  e.  A )
139elpw 3632 . . . . 5  |-  ( { x }  e.  ~P B 
<->  { x }  C_  B )
143snss 3749 . . . . 5  |-  ( x  e.  B  <->  { x }  C_  B )
1513, 14bitr4i 245 . . . 4  |-  ( { x }  e.  ~P B 
<->  x  e.  B )
168, 12, 153imtr3g 262 . . 3  |-  ( ~P A  C_  ~P B  ->  ( x  e.  A  ->  x  e.  B ) )
1716ssrdv 3186 . 2  |-  ( ~P A  C_  ~P B  ->  A  C_  B )
187, 17impbii 182 1  |-  ( A 
C_  B  <->  ~P A  C_ 
~P B )
Colors of variables: wff set class
Syntax hints:    <-> wb 178    e. wcel 1688    C_ wss 3153   ~Pcpw 3626   {csn 3641
This theorem is referenced by:  pwel  4224  ssextss  4226  pweqb  4229  pwdom  7008  marypha1lem  7181  wdompwdom  7287  r1pwss  7451  pwwf  7474  rankpwi  7490  rankxplim  7544  ackbij2lem1  7840  fictb  7866  ssfin2  7941  ssfin3ds  7951  ttukeylem2  8132  hashbclem  11384  wrdexg  11419  incexclem  12289  hashbcss  13045  isacs1i  13553  mreacs  13554  acsfn  13555  sscpwex  13686  wunfunc  13767  isacs3lem  14263  isacs5lem  14266  tgcmp  17122  imastopn  17405  fgabs  17568  fgtr  17579  trfg  17580  ssufl  17607  alexsubb  17734  tsmsres  17820  cfilresi  18715  cmetss  18734  minveclem4a  18788  minveclem4  18790  vitali  18962  sqff1o  20414  ballotlem2  23040  lemindclsbu  25394  neibastop1  25707  neibastop2lem  25708  neibastop2  25709  sstotbnd2  25897  isnacs3  26184  aomclem2  26551
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-14 1692  ax-6 1707  ax-7 1712  ax-11 1719  ax-12 1869  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pr 4213
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1534  df-nf 1537  df-sb 1636  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-v 2791  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-pw 3628  df-sn 3647  df-pr 3648
  Copyright terms: Public domain W3C validator