Theorem pweq 2399

Description: Equality theorem for the power class.

Assertion

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

Proof of Theorem pweq

Step	Hyp	Ref	Expression
1		sseq2 2079	. . 3 |- (A = B -> (x (_ A <-> x (_ B))
2	1	abbidv 1574	. 2 |- (A = B -> {x | x (_ A} = {x | x (_ B})
3		df-pw 2398	. 2 |- P~A = {x | x (_ A}
4		df-pw 2398	. 2 |- P~B = {x | x (_ B}
5	2, 3, 4	3eqtr4g 1528	1 |- (A = B -> P~A = P~B)

Syntax hints:   -> wi 3   = wceq 954  {cab 1461   (_ wss 2043  P~cpw 2397

This theorem is referenced by:  pwex 2740  pwexg 2741  pwssun 2822  canth2g 4471  pwen 4489  pwfi 4551  r1suc 4632  r1val3 4659  ranklim 4665  r1pw 4666  rankxplim 4692  mnfnre 5477  basis1t 7564  eltgt 7568  bastgt 7572  bcth 7982  spwval2 8595  shsspwh 9057  ishgrag 10641  hgralem 10642

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-in 2047  df-ss 2049  df-pw 2398

Copyright terms: Public domain