Theorem pweq 2403

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 2083	. . 3 |- (A = B -> (x (_ A <-> x (_ B))
2	1	abbidv 1577	. 2 |- (A = B -> {x | x (_ A} = {x | x (_ B})
3		df-pw 2402	. 2 |- P~A = {x | x (_ A}
4		df-pw 2402	. 2 |- P~B = {x | x (_ B}
5	2, 3, 4	3eqtr4g 1531	1 |- (A = B -> P~A = P~B)

Syntax hints:   -> wi 3   = wceq 956  {cab 1463   (_ wss 2047  P~cpw 2401

This theorem is referenced by:  pwex 2745  pwexg 2746  pwssun 2827  canth2g 4485  pwen 4503  pwfiOLD 4571  r1suc 4652  r1val3 4679  ranklim 4685  r1pw 4686  rankxplim 4712  mnfnre 5497  basis1t 7614  eltgt 7618  bastgt 7622  bcth 8032  spwval2 8653  shsspwh 9118  sfvlimOLD 10606  limfillem2OLD 10608  ishgrag 10769  hgralem 10770

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-in 2051  df-ss 2053  df-pw 2402

Copyright terms: Public domain