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

Theorem sspwd 4538
Description: The powerclass preserves inclusion (deduction form). (Contributed by BJ, 13-Apr-2024.)
Hypothesis
Ref Expression
sspwd.1 (𝜑𝐴𝐵)
Assertion
Ref Expression
sspwd (𝜑 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

Proof of Theorem sspwd
StepHypRef Expression
1 sspwd.1 . 2 (𝜑𝐴𝐵)
2 sspw 4536 . 2 (𝐴𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
31, 2syl 17 1 (𝜑 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3920  𝒫 cpw 4523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3483  df-in 3927  df-ss 3937  df-pw 4525
This theorem is referenced by:  pweq  4539  pwel  5270  marypha1lem  8895  pwwf  9234  rankpwi  9250  ackbij2lem1  9640  fictb  9666  ssfin2  9741  ssfin3ds  9751  ttukeylem2  9931  hashbcss  16341  isacs1i  16931  mreacs  16932  acsfn  16933  isacs3lem  17779  isacs5lem  17782  tgcmp  22012  imastopn  22331  fgabs  22490  fgtr  22501  trfg  22502  ssufl  22529  alexsubb  22657  cfiluweak  22907  cmetss  23926  minveclem4a  24040  minveclem4  24042  ldsysgenld  31479  neibastop1  33767  neibastop2lem  33768  neibastop2  33769  sstotbnd2  35158  isnacs3  39568  aomclem2  39916  sge0iunmptlemre  42981
  Copyright terms: Public domain W3C validator