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

Theorem sspwb 4536
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 3358 . . . . 5  |-  ( x 
C_  A  ->  ( A  C_  B  ->  x  C_  B ) )
21com12 31 . . . 4  |-  ( A 
C_  B  ->  (
x  C_  A  ->  x 
C_  B ) )
3 vex 2970 . . . . 5  |-  x  e. 
_V
43elpw 3861 . . . 4  |-  ( x  e.  ~P A  <->  x  C_  A
)
53elpw 3861 . . . 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 3357 . 2  |-  ( A 
C_  B  ->  ~P A  C_  ~P B )
8 ssel 3345 . . . 4  |-  ( ~P A  C_  ~P B  ->  ( { x }  e.  ~P A  ->  { x }  e.  ~P B
) )
9 snex 4528 . . . . . 6  |-  { x }  e.  _V
109elpw 3861 . . . . 5  |-  ( { x }  e.  ~P A 
<->  { x }  C_  A )
113snss 3994 . . . . 5  |-  ( x  e.  A  <->  { x }  C_  A )
1210, 11bitr4i 252 . . . 4  |-  ( { x }  e.  ~P A 
<->  x  e.  A )
139elpw 3861 . . . . 5  |-  ( { x }  e.  ~P B 
<->  { x }  C_  B )
143snss 3994 . . . . 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 3357 . 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 1756    C_ wss 3323   ~Pcpw 3855   {csn 3872
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pr 4526
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-v 2969  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-nul 3633  df-pw 3857  df-sn 3873  df-pr 3875
This theorem is referenced by:  pwel  4539  ssextss  4541  pweqb  4544  pwdom  7455  marypha1lem  7675  wdompwdom  7785  r1pwss  7983  pwwf  8006  rankpwi  8022  rankxplim  8078  ackbij2lem1  8380  fictb  8406  ssfin2  8481  ssfin3ds  8491  ttukeylem2  8671  hashbclem  12197  wrdexg  12236  incexclem  13291  hashbcss  14057  isacs1i  14587  mreacs  14588  acsfn  14589  sscpwex  14720  wunfunc  14801  isacs3lem  15328  isacs5lem  15331  tgcmp  18979  imastopn  19268  fgabs  19427  fgtr  19438  trfg  19439  ssufl  19466  alexsubb  19593  tsmsresOLD  19692  tsmsres  19693  cfiluweak  19845  cfilresi  20781  cmetss  20800  minveclem4a  20892  minveclem4  20894  vitali  21068  sqff1o  22495  elsigagen2  26543  measres  26588  imambfm  26629  ballotlem2  26823  neibastop1  28533  neibastop2lem  28534  neibastop2  28535  sstotbnd2  28626  isnacs3  28999  aomclem2  29361
  Copyright terms: Public domain W3C validator