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

Theorem sspwb 4686
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 3496 . . . . 5  |-  ( x 
C_  A  ->  ( A  C_  B  ->  x  C_  B ) )
21com12 31 . . . 4  |-  ( A 
C_  B  ->  (
x  C_  A  ->  x 
C_  B ) )
3 vex 3109 . . . . 5  |-  x  e. 
_V
43elpw 4005 . . . 4  |-  ( x  e.  ~P A  <->  x  C_  A
)
53elpw 4005 . . . 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 3495 . 2  |-  ( A 
C_  B  ->  ~P A  C_  ~P B )
8 ssel 3483 . . . 4  |-  ( ~P A  C_  ~P B  ->  ( { x }  e.  ~P A  ->  { x }  e.  ~P B
) )
9 snex 4678 . . . . . 6  |-  { x }  e.  _V
109elpw 4005 . . . . 5  |-  ( { x }  e.  ~P A 
<->  { x }  C_  A )
113snss 4140 . . . . 5  |-  ( x  e.  A  <->  { x }  C_  A )
1210, 11bitr4i 252 . . . 4  |-  ( { x }  e.  ~P A 
<->  x  e.  A )
139elpw 4005 . . . . 5  |-  ( { x }  e.  ~P B 
<->  { x }  C_  B )
143snss 4140 . . . . 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 3495 . 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 1823    C_ wss 3461   ~Pcpw 3999   {csn 4016
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-sep 4560  ax-nul 4568  ax-pr 4676
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-v 3108  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3784  df-pw 4001  df-sn 4017  df-pr 4019
This theorem is referenced by:  pwel  4689  ssextss  4691  pweqb  4694  pwdom  7662  marypha1lem  7885  wdompwdom  7996  r1pwss  8193  pwwf  8216  rankpwi  8232  rankxplim  8288  ackbij2lem1  8590  fictb  8616  ssfin2  8691  ssfin3ds  8701  ttukeylem2  8881  hashbclem  12485  wrdexg  12544  incexclem  13730  hashbcss  14606  isacs1i  15146  mreacs  15147  acsfn  15148  sscpwex  15303  wunfunc  15387  isacs3lem  15995  isacs5lem  15998  tgcmp  20068  imastopn  20387  fgabs  20546  fgtr  20557  trfg  20558  ssufl  20585  alexsubb  20712  tsmsresOLD  20811  tsmsres  20812  cfiluweak  20964  cfilresi  21900  cmetss  21919  minveclem4a  22011  minveclem4  22013  vitali  22188  sqff1o  23654  elsigagen2  28378  measres  28430  imambfm  28470  ballotlem2  28691  neibastop1  30417  neibastop2lem  30418  neibastop2  30419  sstotbnd2  30510  isnacs3  30882  aomclem2  31240
  Copyright terms: Public domain W3C validator