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

Theorem sspwb 5075
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 3770 . . . . 5 (𝑥𝐴 → (𝐴𝐵𝑥𝐵))
21com12 32 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
3 vex 3353 . . . . 5 𝑥 ∈ V
43elpw 4323 . . . 4 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
53elpw 4323 . . . 4 (𝑥 ∈ 𝒫 𝐵𝑥𝐵)
62, 4, 53imtr4g 287 . . 3 (𝐴𝐵 → (𝑥 ∈ 𝒫 𝐴𝑥 ∈ 𝒫 𝐵))
76ssrdv 3769 . 2 (𝐴𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
8 ssel 3757 . . . 4 (𝒫 𝐴 ⊆ 𝒫 𝐵 → ({𝑥} ∈ 𝒫 𝐴 → {𝑥} ∈ 𝒫 𝐵))
9 snex 5066 . . . . . 6 {𝑥} ∈ V
109elpw 4323 . . . . 5 ({𝑥} ∈ 𝒫 𝐴 ↔ {𝑥} ⊆ 𝐴)
113snss 4472 . . . . 5 (𝑥𝐴 ↔ {𝑥} ⊆ 𝐴)
1210, 11bitr4i 269 . . . 4 ({𝑥} ∈ 𝒫 𝐴𝑥𝐴)
139elpw 4323 . . . . 5 ({𝑥} ∈ 𝒫 𝐵 ↔ {𝑥} ⊆ 𝐵)
143snss 4472 . . . . 5 (𝑥𝐵 ↔ {𝑥} ⊆ 𝐵)
1513, 14bitr4i 269 . . . 4 ({𝑥} ∈ 𝒫 𝐵𝑥𝐵)
168, 12, 153imtr3g 286 . . 3 (𝒫 𝐴 ⊆ 𝒫 𝐵 → (𝑥𝐴𝑥𝐵))
1716ssrdv 3769 . 2 (𝒫 𝐴 ⊆ 𝒫 𝐵𝐴𝐵)
187, 17impbii 200 1 (𝐴𝐵 ↔ 𝒫 𝐴 ⊆ 𝒫 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wb 197  wcel 2155  wss 3734  𝒫 cpw 4317  {csn 4336
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-sep 4943  ax-nul 4951  ax-pr 5064
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-v 3352  df-dif 3737  df-un 3739  df-in 3741  df-ss 3748  df-nul 4082  df-pw 4319  df-sn 4337  df-pr 4339
This theorem is referenced by:  pwel  5078  ssextss  5080  pweqb  5083  pwdom  8323  marypha1lem  8550  wdompwdom  8694  r1pwss  8866  pwwf  8889  rankpwi  8905  rankxplim  8961  ackbij2lem1  9298  fictb  9324  ssfin2  9399  ssfin3ds  9409  ttukeylem2  9589  hashbclem  13442  wrdexg  13501  incexclem  14866  hashbcss  16001  isacs1i  16597  mreacs  16598  acsfn  16599  sscpwex  16754  wunfunc  16838  isacs3lem  17446  isacs5lem  17449  tgcmp  21498  imastopn  21817  fgabs  21976  fgtr  21987  trfg  21988  ssufl  22015  alexsubb  22143  tsmsres  22240  cfiluweak  22392  cfilresi  23386  cmetss  23407  minveclem4a  23504  minveclem4  23506  vitali  23685  sqff1o  25213  elsigagen2  30679  ldsysgenld  30691  ldgenpisyslem1  30694  measres  30753  imambfm  30792  ballotlem2  31019  neibastop1  32818  neibastop2lem  32819  neibastop2  32820  sstotbnd2  34016  psspwb  37952  isnacs3  37975  aomclem2  38326  dssmapnvod  39012  gneispace  39130  sge0less  41270  sge0iunmptlemre  41293
  Copyright terms: Public domain W3C validator