Theorem sspwb 4917

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	⊢ (𝐴 ⊆ 𝐵 ↔ 𝒫 𝐴 ⊆ 𝒫 𝐵)

Proof of Theorem sspwb

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		sstr2 3610	. . . . 5 ⊢ (𝑥 ⊆ 𝐴 → (𝐴 ⊆ 𝐵 → 𝑥 ⊆ 𝐵))
2	1	com12 32	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐵))
3		vex 3203	. . . . 5 ⊢ 𝑥 ∈ V
4	3	elpw 4164	. . . 4 ⊢ (𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴)
5	3	elpw 4164	. . . 4 ⊢ (𝑥 ∈ 𝒫 𝐵 ↔ 𝑥 ⊆ 𝐵)
6	2, 4, 5	3imtr4g 285	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵))
7	6	ssrdv 3609	. 2 ⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
8		ssel 3597	. . . 4 ⊢ (𝒫 𝐴 ⊆ 𝒫 𝐵 → ({𝑥} ∈ 𝒫 𝐴 → {𝑥} ∈ 𝒫 𝐵))
9		snex 4908	. . . . . 6 ⊢ {𝑥} ∈ V
10	9	elpw 4164	. . . . 5 ⊢ ({𝑥} ∈ 𝒫 𝐴 ↔ {𝑥} ⊆ 𝐴)
11	3	snss 4316	. . . . 5 ⊢ (𝑥 ∈ 𝐴 ↔ {𝑥} ⊆ 𝐴)
12	10, 11	bitr4i 267	. . . 4 ⊢ ({𝑥} ∈ 𝒫 𝐴 ↔ 𝑥 ∈ 𝐴)
13	9	elpw 4164	. . . . 5 ⊢ ({𝑥} ∈ 𝒫 𝐵 ↔ {𝑥} ⊆ 𝐵)
14	3	snss 4316	. . . . 5 ⊢ (𝑥 ∈ 𝐵 ↔ {𝑥} ⊆ 𝐵)
15	13, 14	bitr4i 267	. . . 4 ⊢ ({𝑥} ∈ 𝒫 𝐵 ↔ 𝑥 ∈ 𝐵)
16	8, 12, 15	3imtr3g 284	. . 3 ⊢ (𝒫 𝐴 ⊆ 𝒫 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
17	16	ssrdv 3609	. 2 ⊢ (𝒫 𝐴 ⊆ 𝒫 𝐵 → 𝐴 ⊆ 𝐵)
18	7, 17	impbii 199	1 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝒫 𝐴 ⊆ 𝒫 𝐵)

Syntax hints:   ↔ wb 196   ∈ wcel 1990   ⊆ wss 3574  𝒫 cpw 4158  {csn 4177

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-pw 4160  df-sn 4178  df-pr 4180

This theorem is referenced by:  pwel  4920  ssextss  4922  pweqb  4925  pwdom  8112  marypha1lem  8339  wdompwdom  8483  r1pwss  8647  pwwf  8670  rankpwi  8686  rankxplim  8742  ackbij2lem1  9041  fictb  9067  ssfin2  9142  ssfin3ds  9152  ttukeylem2  9332  hashbclem  13236  wrdexg  13315  incexclem  14568  hashbcss  15708  isacs1i  16318  mreacs  16319  acsfn  16320  sscpwex  16475  wunfunc  16559  isacs3lem  17166  isacs5lem  17169  tgcmp  21204  imastopn  21523  fgabs  21683  fgtr  21694  trfg  21695  ssufl  21722  alexsubb  21850  tsmsres  21947  cfiluweak  22099  cfilresi  23093  cmetss  23113  minveclem4a  23201  minveclem4  23203  vitali  23382  sqff1o  24908  elsigagen2  30211  ldsysgenld  30223  ldgenpisyslem1  30226  measres  30285  imambfm  30324  ballotlem2  30550  neibastop1  32354  neibastop2lem  32355  neibastop2  32356  sstotbnd2  33573  isnacs3  37273  aomclem2  37625  dssmapnvod  38314  gneispace  38432  sge0less  40609  sge0iunmptlemre  40632