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.

Step	Hyp	Ref	Expression
1		sstr2 3496	. . . . 5 |- ( x C_ A -> ( A C_ B -> x C_ B ) )
2	1	com12 31	. . . 4 |- ( A C_ B -> ( x C_ A -> x C_ B ) )
3		vex 3109	. . . . 5 |- x e. _V
4	3	elpw 4005	. . . 4 |- ( x e. ~P A <-> x C_ A )
5	3	elpw 4005	. . . 4 |- ( x e. ~P B <-> x C_ B )
6	2, 4, 5	3imtr4g 270	. . 3 |- ( A C_ B -> ( x e. ~P A -> x e. ~P B ) )
7	6	ssrdv 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
10	9	elpw 4005	. . . . 5 |- ( { x } e. ~P A <-> { x } C_ A )
11	3	snss 4140	. . . . 5 |- ( x e. A <-> { x } C_ A )
12	10, 11	bitr4i 252	. . . 4 |- ( { x } e. ~P A <-> x e. A )
13	9	elpw 4005	. . . . 5 |- ( { x } e. ~P B <-> { x } C_ B )
14	3	snss 4140	. . . . 5 |- ( x e. B <-> { x } C_ B )
15	13, 14	bitr4i 252	. . . 4 |- ( { x } e. ~P B <-> x e. B )
16	8, 12, 15	3imtr3g 269	. . 3 |- ( ~P A C_ ~P B -> ( x e. A -> x e. B ) )
17	16	ssrdv 3495	. 2 |- ( ~P A C_ ~P B -> A C_ B )
18	7, 17	impbii 188	1 |- ( A C_ B <-> ~P A C_ ~P B )

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