Theorem sspwd 4569

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3895  𝒫 cpw 4556

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-pw 4558

This theorem is used by:  pweq  4570  pwel  5342  pwuninel  8292  marypha1lem  9425  pwwf  9815  rankpwi  9832  ackbij2lem1  10296  fictb  10322  ssfin2  10398  ssfin3ds  10408  ttukeylem2  10588  hashbcss  17182  isacs1i  17831  mreacs  17832  acsfn  17833  isacs3lem  18716  isacs5lem  18719  tgcmp  23719  imastopn  24039  fgabs  24198  fgtr  24209  trfg  24210  ssufl  24237  alexsubb  24365  cfiluweak  24613  cmetss  25637  minveclem4a  25751  minveclem4  25753  madess  28252  ldsysgenld  34793  neibastop1  37147  neibastop2lem  37148  neibastop2  37149  sstotbnd2  38709  isnacs3  43721  aomclem2  44057  sge0iunmptlemre  47425