Theorem sspwb 4652

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 3474	. . . . 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 3081	. . . . 5 |- x e. _V
4	3	elpw 3977	. . . 4 |- ( x e. ~P A <-> x C_ A )
5	3	elpw 3977	. . . 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 3473	. 2 |- ( A C_ B -> ~P A C_ ~P B )
8		ssel 3461	. . . 4 |- ( ~P A C_ ~P B -> ( { x } e. ~P A -> { x } e. ~P B ) )
9		snex 4644	. . . . . 6 |- { x } e. _V
10	9	elpw 3977	. . . . 5 |- ( { x } e. ~P A <-> { x } C_ A )
11	3	snss 4110	. . . . 5 |- ( x e. A <-> { x } C_ A )
12	10, 11	bitr4i 252	. . . 4 |- ( { x } e. ~P A <-> x e. A )
13	9	elpw 3977	. . . . 5 |- ( { x } e. ~P B <-> { x } C_ B )
14	3	snss 4110	. . . . 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 3473	. 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 1758   C_ wss 3439   ~Pcpw 3971   {csn 3988

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4524  ax-nul 4532  ax-pr 4642

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-v 3080  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-pw 3973  df-sn 3989  df-pr 3991

This theorem is referenced by:  pwel  4655  ssextss  4657  pweqb  4660  pwdom  7576  marypha1lem  7797  wdompwdom  7907  r1pwss  8105  pwwf  8128  rankpwi  8144  rankxplim  8200  ackbij2lem1  8502  fictb  8528  ssfin2  8603  ssfin3ds  8613  ttukeylem2  8793  hashbclem  12326  wrdexg  12365  incexclem  13420  hashbcss  14186  isacs1i  14717  mreacs  14718  acsfn  14719  sscpwex  14850  wunfunc  14931  isacs3lem  15458  isacs5lem  15461  tgcmp  19139  imastopn  19428  fgabs  19587  fgtr  19598  trfg  19599  ssufl  19626  alexsubb  19753  tsmsresOLD  19852  tsmsres  19853  cfiluweak  20005  cfilresi  20941  cmetss  20960  minveclem4a  21052  minveclem4  21054  vitali  21229  sqff1o  22656  elsigagen2  26756  measres  26801  imambfm  26841  ballotlem2  27035  neibastop1  28748  neibastop2lem  28749  neibastop2  28750  sstotbnd2  28841  isnacs3  29214  aomclem2  29576