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

Theorem sspwb 4415
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 3357 . . . . 5  |-  ( x 
C_  A  ->  ( A  C_  B  ->  x  C_  B ) )
21com12 30 . . . 4  |-  ( A 
C_  B  ->  (
x  C_  A  ->  x 
C_  B ) )
3 vex 2961 . . . . 5  |-  x  e. 
_V
43elpw 3807 . . . 4  |-  ( x  e.  ~P A  <->  x  C_  A
)
53elpw 3807 . . . 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 3356 . 2  |-  ( A 
C_  B  ->  ~P A  C_  ~P B )
8 ssel 3344 . . . 4  |-  ( ~P A  C_  ~P B  ->  ( { x }  e.  ~P A  ->  { x }  e.  ~P B
) )
9 snex 4407 . . . . . 6  |-  { x }  e.  _V
109elpw 3807 . . . . 5  |-  ( { x }  e.  ~P A 
<->  { x }  C_  A )
113snss 3928 . . . . 5  |-  ( x  e.  A  <->  { x }  C_  A )
1210, 11bitr4i 245 . . . 4  |-  ( { x }  e.  ~P A 
<->  x  e.  A )
139elpw 3807 . . . . 5  |-  ( { x }  e.  ~P B 
<->  { x }  C_  B )
143snss 3928 . . . . 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 3356 . 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 1726    C_ wss 3322   ~Pcpw 3801   {csn 3816
This theorem is referenced by:  pwel  4417  ssextss  4419  pweqb  4422  pwdom  7261  marypha1lem  7440  wdompwdom  7548  r1pwss  7712  pwwf  7735  rankpwi  7751  rankxplim  7805  ackbij2lem1  8101  fictb  8127  ssfin2  8202  ssfin3ds  8212  ttukeylem2  8392  hashbclem  11703  wrdexg  11741  incexclem  12618  hashbcss  13374  isacs1i  13884  mreacs  13885  acsfn  13886  sscpwex  14017  wunfunc  14098  isacs3lem  14594  isacs5lem  14597  tgcmp  17466  imastopn  17754  fgabs  17913  fgtr  17924  trfg  17925  ssufl  17952  alexsubb  18079  tsmsres  18175  cfiluweak  18327  cfilresi  19250  cmetss  19269  minveclem4a  19333  minveclem4  19335  vitali  19507  sqff1o  20967  elsigagen2  24533  measres  24578  imambfm  24614  ballotlem2  24748  neibastop1  26390  neibastop2lem  26391  neibastop2  26392  sstotbnd2  26485  isnacs3  26766  aomclem2  27132
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 2419  ax-sep 4332  ax-nul 4340  ax-pr 4405
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-v 2960  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-nul 3631  df-pw 3803  df-sn 3822  df-pr 3823
  Copyright terms: Public domain W3C validator