Theorem pweq 2407

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 2086	. . 3 |- (A = B -> (x (_ A <-> x (_ B))
2	1	abbidv 1580	. 2 |- (A = B -> {x | x (_ A} = {x | x (_ B})
3		df-pw 2406	. 2 |- P~A = {x | x (_ A}
4		df-pw 2406	. 2 |- P~B = {x | x (_ B}
5	2, 3, 4	3eqtr4g 1534	1 |- (A = B -> P~A = P~B)

Syntax hints:   -> wi 3   = wceq 958  {cab 1466   (_ wss 2050  P~cpw 2405

This theorem is referenced by:  pwex 2751  pwexg 2752  pwssun 2833  canth2g 4491  pwen 4509  pwfi 4579  pwfiOLD 4580  r1suc 4662  r1val3 4689  ranklim 4695  r1pw 4696  rankxplim 4722  mnfnre 5509  basis1t 7613  eltgt 7617  bastgt 7621  bcth 8029  spwval2 8649  shsspwh 9113  sfvlimOLD 10577  limfillem2OLD 10579  ishgrag 10740  hgralem 10741

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-in 2054  df-ss 2056  df-pw 2406

Copyright terms: Public domain