Theorem sspwd 4573

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 4571	. 2 ⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)
3	1, 2	syl 18	1 ⊢ (𝜑 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3900  𝒫 cpw 4560

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-pw 4562

This theorem is used by:  pweq  4574  pwel  5347  pwuninel  8317  marypha1lem  9449  pwwf  9839  rankpwi  9856  ackbij2lem1  10320  fictb  10346  ssfin2  10422  ssfin3ds  10432  ttukeylem2  10612  hashbcss  17208  isacs1i  17857  mreacs  17858  acsfn  17859  isacs3lem  18742  isacs5lem  18745  tgcmp  23746  imastopn  24066  fgabs  24225  fgtr  24236  trfg  24237  ssufl  24264  alexsubb  24392  cfiluweak  24640  cmetss  25664  minveclem4a  25778  minveclem4  25780  madess  28279  ldsysgenld  34860  neibastop1  37324  neibastop2lem  37325  neibastop2  37326  sstotbnd2  38899  isnacs3  43912  aomclem2  44248  sge0iunmptlemre  47628