Theorem sspwd 4570

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

Step	Hyp	Ref	Expression
1		sspwd.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		sspw 4568	. 2 ⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
3	1, 2	syl 18	1 ⊢ (𝜑 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3899  𝒫 cpw 4557

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3916  df-pw 4559

This theorem is used by:  pweq  4571  pwel  5346  pwuninel  8278  marypha1lem  9410  pwwf  9796  rankpwi  9812  ackbij2lem1  10245  fictb  10271  ssfin2  10347  ssfin3ds  10357  ttukeylem2  10537  hashbcss  17121  isacs1i  17770  mreacs  17771  acsfn  17772  isacs3lem  18655  isacs5lem  18658  tgcmp  23658  imastopn  23978  fgabs  24137  fgtr  24148  trfg  24149  ssufl  24176  alexsubb  24304  cfiluweak  24552  cmetss  25576  minveclem4a  25690  minveclem4  25692  madess  28163  ldsysgenld  34704  neibastop1  37045  neibastop2lem  37046  neibastop2  37047  sstotbnd2  38589  prjcrv0  43544  isnacs3  43620  aomclem2  43961  sge0iunmptlemre  47308