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

Theorem sspwb 4622
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 3407 . . . . 5  |-  ( x 
C_  A  ->  ( A  C_  B  ->  x  C_  B ) )
21com12 32 . . . 4  |-  ( A 
C_  B  ->  (
x  C_  A  ->  x 
C_  B ) )
3 vex 3016 . . . . 5  |-  x  e. 
_V
43elpw 3925 . . . 4  |-  ( x  e.  ~P A  <->  x  C_  A
)
53elpw 3925 . . . 4  |-  ( x  e.  ~P B  <->  x  C_  B
)
62, 4, 53imtr4g 278 . . 3  |-  ( A 
C_  B  ->  (
x  e.  ~P A  ->  x  e.  ~P B
) )
76ssrdv 3406 . 2  |-  ( A 
C_  B  ->  ~P A  C_  ~P B )
8 ssel 3394 . . . 4  |-  ( ~P A  C_  ~P B  ->  ( { x }  e.  ~P A  ->  { x }  e.  ~P B
) )
9 snex 4614 . . . . . 6  |-  { x }  e.  _V
109elpw 3925 . . . . 5  |-  ( { x }  e.  ~P A 
<->  { x }  C_  A )
113snss 4065 . . . . 5  |-  ( x  e.  A  <->  { x }  C_  A )
1210, 11bitr4i 260 . . . 4  |-  ( { x }  e.  ~P A 
<->  x  e.  A )
139elpw 3925 . . . . 5  |-  ( { x }  e.  ~P B 
<->  { x }  C_  B )
143snss 4065 . . . . 5  |-  ( x  e.  B  <->  { x }  C_  B )
1513, 14bitr4i 260 . . . 4  |-  ( { x }  e.  ~P B 
<->  x  e.  B )
168, 12, 153imtr3g 277 . . 3  |-  ( ~P A  C_  ~P B  ->  ( x  e.  A  ->  x  e.  B ) )
1716ssrdv 3406 . 2  |-  ( ~P A  C_  ~P B  ->  A  C_  B )
187, 17impbii 192 1  |-  ( A 
C_  B  <->  ~P A  C_ 
~P B )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189    e. wcel 1891    C_ wss 3372   ~Pcpw 3919   {csn 3936
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-9 1900  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432  ax-sep 4497  ax-nul 4506  ax-pr 4612
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 988  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-ne 2624  df-v 3015  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-nul 3700  df-pw 3921  df-sn 3937  df-pr 3939
This theorem is referenced by:  pwel  4625  ssextss  4627  pweqb  4630  pwdom  7711  marypha1lem  7934  wdompwdom  8080  r1pwss  8242  pwwf  8265  rankpwi  8281  rankxplim  8337  ackbij2lem1  8636  fictb  8662  ssfin2  8737  ssfin3ds  8747  ttukeylem2  8927  hashbclem  12610  wrdexg  12677  incexclem  13905  hashbcss  14967  isacs1i  15574  mreacs  15575  acsfn  15576  sscpwex  15731  wunfunc  15815  isacs3lem  16423  isacs5lem  16426  tgcmp  20427  imastopn  20746  fgabs  20905  fgtr  20916  trfg  20917  ssufl  20944  alexsubb  21072  tsmsres  21169  cfiluweak  21321  cfilresi  22276  cmetss  22295  minveclem4a  22383  minveclem4  22385  minveclem4aOLD  22395  minveclem4OLD  22397  vitali  22583  sqff1o  24121  elsigagen2  28977  ldsysgenld  28989  ldgenpisyslem1  28992  measres  29051  imambfm  29090  ballotlem2  29327  neibastop1  31021  neibastop2lem  31022  neibastop2  31023  sstotbnd2  32108  isnacs3  35554  aomclem2  35915  sge0less  38293  sge0iunmptlemre  38316
  Copyright terms: Public domain W3C validator