MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sspwb Structured version   Visualization version   GIF version

Theorem sspwb 4834
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.
StepHypRef Expression
1 sstr2 3570 . . . . 5 (𝑥𝐴 → (𝐴𝐵𝑥𝐵))
21com12 32 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
3 vex 3171 . . . . 5 𝑥 ∈ V
43elpw 4109 . . . 4 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
53elpw 4109 . . . 4 (𝑥 ∈ 𝒫 𝐵𝑥𝐵)
62, 4, 53imtr4g 283 . . 3 (𝐴𝐵 → (𝑥 ∈ 𝒫 𝐴𝑥 ∈ 𝒫 𝐵))
76ssrdv 3569 . 2 (𝐴𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
8 ssel 3557 . . . 4 (𝒫 𝐴 ⊆ 𝒫 𝐵 → ({𝑥} ∈ 𝒫 𝐴 → {𝑥} ∈ 𝒫 𝐵))
9 snex 4826 . . . . . 6 {𝑥} ∈ V
109elpw 4109 . . . . 5 ({𝑥} ∈ 𝒫 𝐴 ↔ {𝑥} ⊆ 𝐴)
113snss 4254 . . . . 5 (𝑥𝐴 ↔ {𝑥} ⊆ 𝐴)
1210, 11bitr4i 265 . . . 4 ({𝑥} ∈ 𝒫 𝐴𝑥𝐴)
139elpw 4109 . . . . 5 ({𝑥} ∈ 𝒫 𝐵 ↔ {𝑥} ⊆ 𝐵)
143snss 4254 . . . . 5 (𝑥𝐵 ↔ {𝑥} ⊆ 𝐵)
1513, 14bitr4i 265 . . . 4 ({𝑥} ∈ 𝒫 𝐵𝑥𝐵)
168, 12, 153imtr3g 282 . . 3 (𝒫 𝐴 ⊆ 𝒫 𝐵 → (𝑥𝐴𝑥𝐵))
1716ssrdv 3569 . 2 (𝒫 𝐴 ⊆ 𝒫 𝐵𝐴𝐵)
187, 17impbii 197 1 (𝐴𝐵 ↔ 𝒫 𝐴 ⊆ 𝒫 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 194  wcel 1975  wss 3535  𝒫 cpw 4103  {csn 4120
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2228  ax-ext 2585  ax-sep 4699  ax-nul 4708  ax-pr 4824
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-clab 2592  df-cleq 2598  df-clel 2601  df-nfc 2735  df-v 3170  df-dif 3538  df-un 3540  df-in 3542  df-ss 3549  df-nul 3870  df-pw 4105  df-sn 4121  df-pr 4123
This theorem is referenced by:  pwel  4837  ssextss  4839  pweqb  4842  pwdom  7970  marypha1lem  8195  wdompwdom  8339  r1pwss  8503  pwwf  8526  rankpwi  8542  rankxplim  8598  ackbij2lem1  8897  fictb  8923  ssfin2  8998  ssfin3ds  9008  ttukeylem2  9188  hashbclem  13041  wrdexg  13112  incexclem  14349  hashbcss  15488  isacs1i  16083  mreacs  16084  acsfn  16085  sscpwex  16240  wunfunc  16324  isacs3lem  16931  isacs5lem  16934  tgcmp  20952  imastopn  21271  fgabs  21431  fgtr  21442  trfg  21443  ssufl  21470  alexsubb  21598  tsmsres  21695  cfiluweak  21847  cfilresi  22815  cmetss  22834  minveclem4a  22922  minveclem4  22924  vitali  23101  sqff1o  24621  elsigagen2  29340  ldsysgenld  29352  ldgenpisyslem1  29355  measres  29414  imambfm  29453  ballotlem2  29679  neibastop1  31326  neibastop2lem  31327  neibastop2  31328  sstotbnd2  32542  isnacs3  36090  aomclem2  36442  dssmapnvod  37133  gneispace  37251  sge0less  39085  sge0iunmptlemre  39108
  Copyright terms: Public domain W3C validator