Theorem pweqd 3654

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

Hypothesis

Ref	Expression
pweqd.1	|- ( ph -> A = B )

Assertion

Ref	Expression
pweqd	|- ( ph -> ~P A = ~P B )

Proof of Theorem pweqd

Step	Hyp	Ref	Expression
1		pweqd.1	. 2 |- ( ph -> A = B )
2		pweq 3652	. 2 |- ( A = B -> ~P A = ~P B )
3	1, 2	syl 14	1 |- ( ph -> ~P A = ~P B )

Syntax hints:   -> wi 4   = wceq 1395   ~Pcpw 3649

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210  df-pw 3651

This theorem is referenced by:  pmvalg  6806  issubm  13505  issubg  13710  subgex  13713  issubrng  14163  issubrg  14185  lsssetm  14320  lspfval  14352  lsppropd  14396  sraval  14401  basis1  14721  baspartn  14724  cldval  14773  ntrfval  14774  clsfval  14775  neifval  14814  mopnfss  15121  isuhgrm  15871  isushgrm  15872  isuhgropm  15881  uhgrun  15886  isupgren  15895  upgrop  15904  isumgren  15905  upgrun  15924  umgrun  15926  isuspgren  15955  isusgren  15956  isuspgropen  15962  isusgropen  15963  ausgrusgrben  15966  usgrstrrepeen  16029