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

Theorem sspwb 4652
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 3474 . . . . 5  |-  ( x 
C_  A  ->  ( A  C_  B  ->  x  C_  B ) )
21com12 31 . . . 4  |-  ( A 
C_  B  ->  (
x  C_  A  ->  x 
C_  B ) )
3 vex 3081 . . . . 5  |-  x  e. 
_V
43elpw 3977 . . . 4  |-  ( x  e.  ~P A  <->  x  C_  A
)
53elpw 3977 . . . 4  |-  ( x  e.  ~P B  <->  x  C_  B
)
62, 4, 53imtr4g 270 . . 3  |-  ( A 
C_  B  ->  (
x  e.  ~P A  ->  x  e.  ~P B
) )
76ssrdv 3473 . 2  |-  ( A 
C_  B  ->  ~P A  C_  ~P B )
8 ssel 3461 . . . 4  |-  ( ~P A  C_  ~P B  ->  ( { x }  e.  ~P A  ->  { x }  e.  ~P B
) )
9 snex 4644 . . . . . 6  |-  { x }  e.  _V
109elpw 3977 . . . . 5  |-  ( { x }  e.  ~P A 
<->  { x }  C_  A )
113snss 4110 . . . . 5  |-  ( x  e.  A  <->  { x }  C_  A )
1210, 11bitr4i 252 . . . 4  |-  ( { x }  e.  ~P A 
<->  x  e.  A )
139elpw 3977 . . . . 5  |-  ( { x }  e.  ~P B 
<->  { x }  C_  B )
143snss 4110 . . . . 5  |-  ( x  e.  B  <->  { x }  C_  B )
1513, 14bitr4i 252 . . . 4  |-  ( { x }  e.  ~P B 
<->  x  e.  B )
168, 12, 153imtr3g 269 . . 3  |-  ( ~P A  C_  ~P B  ->  ( x  e.  A  ->  x  e.  B ) )
1716ssrdv 3473 . 2  |-  ( ~P A  C_  ~P B  ->  A  C_  B )
187, 17impbii 188 1  |-  ( A 
C_  B  <->  ~P A  C_ 
~P B )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    e. wcel 1758    C_ wss 3439   ~Pcpw 3971   {csn 3988
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4524  ax-nul 4532  ax-pr 4642
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-v 3080  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-pw 3973  df-sn 3989  df-pr 3991
This theorem is referenced by:  pwel  4655  ssextss  4657  pweqb  4660  pwdom  7576  marypha1lem  7797  wdompwdom  7907  r1pwss  8105  pwwf  8128  rankpwi  8144  rankxplim  8200  ackbij2lem1  8502  fictb  8528  ssfin2  8603  ssfin3ds  8613  ttukeylem2  8793  hashbclem  12326  wrdexg  12365  incexclem  13420  hashbcss  14186  isacs1i  14717  mreacs  14718  acsfn  14719  sscpwex  14850  wunfunc  14931  isacs3lem  15458  isacs5lem  15461  tgcmp  19139  imastopn  19428  fgabs  19587  fgtr  19598  trfg  19599  ssufl  19626  alexsubb  19753  tsmsresOLD  19852  tsmsres  19853  cfiluweak  20005  cfilresi  20941  cmetss  20960  minveclem4a  21052  minveclem4  21054  vitali  21229  sqff1o  22656  elsigagen2  26756  measres  26801  imambfm  26841  ballotlem2  27035  neibastop1  28748  neibastop2lem  28749  neibastop2  28750  sstotbnd2  28841  isnacs3  29214  aomclem2  29576
  Copyright terms: Public domain W3C validator