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

Theorem sspwb 4908
 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 3602 . . . . 5 (𝑥𝐴 → (𝐴𝐵𝑥𝐵))
21com12 32 . . . 4 (𝐴𝐵 → (𝑥𝐴𝑥𝐵))
3 vex 3198 . . . . 5 𝑥 ∈ V
43elpw 4155 . . . 4 (𝑥 ∈ 𝒫 𝐴𝑥𝐴)
53elpw 4155 . . . 4 (𝑥 ∈ 𝒫 𝐵𝑥𝐵)
62, 4, 53imtr4g 285 . . 3 (𝐴𝐵 → (𝑥 ∈ 𝒫 𝐴𝑥 ∈ 𝒫 𝐵))
76ssrdv 3601 . 2 (𝐴𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
8 ssel 3589 . . . 4 (𝒫 𝐴 ⊆ 𝒫 𝐵 → ({𝑥} ∈ 𝒫 𝐴 → {𝑥} ∈ 𝒫 𝐵))
9 snex 4899 . . . . . 6 {𝑥} ∈ V
109elpw 4155 . . . . 5 ({𝑥} ∈ 𝒫 𝐴 ↔ {𝑥} ⊆ 𝐴)
113snss 4307 . . . . 5 (𝑥𝐴 ↔ {𝑥} ⊆ 𝐴)
1210, 11bitr4i 267 . . . 4 ({𝑥} ∈ 𝒫 𝐴𝑥𝐴)
139elpw 4155 . . . . 5 ({𝑥} ∈ 𝒫 𝐵 ↔ {𝑥} ⊆ 𝐵)
143snss 4307 . . . . 5 (𝑥𝐵 ↔ {𝑥} ⊆ 𝐵)
1513, 14bitr4i 267 . . . 4 ({𝑥} ∈ 𝒫 𝐵𝑥𝐵)
168, 12, 153imtr3g 284 . . 3 (𝒫 𝐴 ⊆ 𝒫 𝐵 → (𝑥𝐴𝑥𝐵))
1716ssrdv 3601 . 2 (𝒫 𝐴 ⊆ 𝒫 𝐵𝐴𝐵)
187, 17impbii 199 1 (𝐴𝐵 ↔ 𝒫 𝐴 ⊆ 𝒫 𝐵)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196   ∈ wcel 1988   ⊆ wss 3567  𝒫 cpw 4149  {csn 4168 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-pw 4151  df-sn 4169  df-pr 4171 This theorem is referenced by:  pwel  4911  ssextss  4913  pweqb  4916  pwdom  8097  marypha1lem  8324  wdompwdom  8468  r1pwss  8632  pwwf  8655  rankpwi  8671  rankxplim  8727  ackbij2lem1  9026  fictb  9052  ssfin2  9127  ssfin3ds  9137  ttukeylem2  9317  hashbclem  13219  wrdexg  13298  incexclem  14549  hashbcss  15689  isacs1i  16299  mreacs  16300  acsfn  16301  sscpwex  16456  wunfunc  16540  isacs3lem  17147  isacs5lem  17150  tgcmp  21185  imastopn  21504  fgabs  21664  fgtr  21675  trfg  21676  ssufl  21703  alexsubb  21831  tsmsres  21928  cfiluweak  22080  cfilresi  23074  cmetss  23094  minveclem4a  23182  minveclem4  23184  vitali  23363  sqff1o  24889  elsigagen2  30185  ldsysgenld  30197  ldgenpisyslem1  30200  measres  30259  imambfm  30298  ballotlem2  30524  neibastop1  32329  neibastop2lem  32330  neibastop2  32331  sstotbnd2  33544  isnacs3  37092  aomclem2  37444  dssmapnvod  38134  gneispace  38252  sge0less  40372  sge0iunmptlemre  40395
 Copyright terms: Public domain W3C validator