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

Theorem sspwb 4405
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 3347 . . . . 5  |-  ( x 
C_  A  ->  ( A  C_  B  ->  x  C_  B ) )
21com12 29 . . . 4  |-  ( A 
C_  B  ->  (
x  C_  A  ->  x 
C_  B ) )
3 vex 2951 . . . . 5  |-  x  e. 
_V
43elpw 3797 . . . 4  |-  ( x  e.  ~P A  <->  x  C_  A
)
53elpw 3797 . . . 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 3346 . 2  |-  ( A 
C_  B  ->  ~P A  C_  ~P B )
8 ssel 3334 . . . 4  |-  ( ~P A  C_  ~P B  ->  ( { x }  e.  ~P A  ->  { x }  e.  ~P B
) )
9 snex 4397 . . . . . 6  |-  { x }  e.  _V
109elpw 3797 . . . . 5  |-  ( { x }  e.  ~P A 
<->  { x }  C_  A )
113snss 3918 . . . . 5  |-  ( x  e.  A  <->  { x }  C_  A )
1210, 11bitr4i 244 . . . 4  |-  ( { x }  e.  ~P A 
<->  x  e.  A )
139elpw 3797 . . . . 5  |-  ( { x }  e.  ~P B 
<->  { x }  C_  B )
143snss 3918 . . . . 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 3346 . 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 1725    C_ wss 3312   ~Pcpw 3791   {csn 3806
This theorem is referenced by:  pwel  4407  ssextss  4409  pweqb  4412  pwdom  7251  marypha1lem  7430  wdompwdom  7538  r1pwss  7702  pwwf  7725  rankpwi  7741  rankxplim  7795  ackbij2lem1  8091  fictb  8117  ssfin2  8192  ssfin3ds  8202  ttukeylem2  8382  hashbclem  11693  wrdexg  11731  incexclem  12608  hashbcss  13364  isacs1i  13874  mreacs  13875  acsfn  13876  sscpwex  14007  wunfunc  14088  isacs3lem  14584  isacs5lem  14587  tgcmp  17456  imastopn  17744  fgabs  17903  fgtr  17914  trfg  17915  ssufl  17942  alexsubb  18069  tsmsres  18165  cfiluweak  18317  cfilresi  19240  cmetss  19259  minveclem4a  19323  minveclem4  19325  vitali  19497  sqff1o  20957  elsigagen2  24523  measres  24568  imambfm  24604  ballotlem2  24738  neibastop1  26379  neibastop2lem  26380  neibastop2  26381  sstotbnd2  26474  isnacs3  26755  aomclem2  27121
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pr 4395
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-pw 3793  df-sn 3812  df-pr 3813
  Copyright terms: Public domain W3C validator