Theorem pweqd 3673

Description: Equality deduction for power class. (Contributed by NM, 27-Nov-2013.)

Hypothesis

Ref	Expression
pweqd.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
pweqd	⊢ (𝜑 → 𝒫 𝐴 = 𝒫 𝐵)

Proof of Theorem pweqd

Step	Hyp	Ref	Expression
1		pweqd.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		pweq 3671	. 2 ⊢ (𝐴 = 𝐵 → 𝒫 𝐴 = 𝒫 𝐵)
3	1, 2	syl 14	1 ⊢ (𝜑 → 𝒫 𝐴 = 𝒫 𝐵)

Syntax hints:   → wi 4   = wceq 1398  𝒫 cpw 3668

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3216  df-ss 3223  df-pw 3670

This theorem is referenced by:  pmvalg  6892  issubm  13677  issubg  13882  subgex  13885  issubrng  14336  issubrg  14358  lsssetm  14496  lspfval  14528  lsppropd  14572  sraval  14577  basis1  14904  baspartn  14907  cldval  14956  ntrfval  14957  clsfval  14958  neifval  14997  mopnfss  15304  isuhgrm  16058  isushgrm  16059  isuhgropm  16068  uhgrun  16073  isupgren  16082  upgrop  16091  isumgren  16092  umgr1een  16112  upgrun  16113  umgrun  16115  isuspgren  16144  isusgren  16145  isuspgropen  16151  isusgropen  16152  ausgrusgrben  16155  usgrstrrepeen  16218  issubgr  16244  uhgrspansubgrlem  16263