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.

Step	Hyp	Ref	Expression
1		sstr2 3358	. . . . 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 2970	. . . . 5 |- x e. _V
4	3	elpw 3861	. . . 4 |- ( x e. ~P A <-> x C_ A )
5	3	elpw 3861	. . . 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 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
10	9	elpw 3861	. . . . 5 |- ( { x } e. ~P A <-> { x } C_ A )
11	3	snss 3994	. . . . 5 |- ( x e. A <-> { x } C_ A )
12	10, 11	bitr4i 252	. . . 4 |- ( { x } e. ~P A <-> x e. A )
13	9	elpw 3861	. . . . 5 |- ( { x } e. ~P B <-> { x } C_ B )
14	3	snss 3994	. . . . 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 3357	. 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 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