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.

Step	Hyp	Ref	Expression
1		sstr2 3407	. . . . 5 |- ( x C_ A -> ( A C_ B -> x C_ B ) )
2	1	com12 32	. . . 4 |- ( A C_ B -> ( x C_ A -> x C_ B ) )
3		vex 3016	. . . . 5 |- x e. _V
4	3	elpw 3925	. . . 4 |- ( x e. ~P A <-> x C_ A )
5	3	elpw 3925	. . . 4 |- ( x e. ~P B <-> x C_ B )
6	2, 4, 5	3imtr4g 278	. . 3 |- ( A C_ B -> ( x e. ~P A -> x e. ~P B ) )
7	6	ssrdv 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
10	9	elpw 3925	. . . . 5 |- ( { x } e. ~P A <-> { x } C_ A )
11	3	snss 4065	. . . . 5 |- ( x e. A <-> { x } C_ A )
12	10, 11	bitr4i 260	. . . 4 |- ( { x } e. ~P A <-> x e. A )
13	9	elpw 3925	. . . . 5 |- ( { x } e. ~P B <-> { x } C_ B )
14	3	snss 4065	. . . . 5 |- ( x e. B <-> { x } C_ B )
15	13, 14	bitr4i 260	. . . 4 |- ( { x } e. ~P B <-> x e. B )
16	8, 12, 15	3imtr3g 277	. . 3 |- ( ~P A C_ ~P B -> ( x e. A -> x e. B ) )
17	16	ssrdv 3406	. 2 |- ( ~P A C_ ~P B -> A C_ B )
18	7, 17	impbii 192	1 |- ( A C_ B <-> ~P A C_ ~P B )

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