Theorem pweq 2460

Description: Equality theorem for the power class.

Assertion

Ref	Expression
pweq	⊢ (A = B → ℘A = ℘B)

Proof of Theorem pweq

Step	Hyp	Ref	Expression
1		sseq2 2135	. . 3 ⊢ (A = B → (x ⊆ A ↔ x ⊆ B))
2	1	abbidv 1620	. 2 ⊢ (A = B → {x∣x ⊆ A} = {x∣x ⊆ B})
3		df-pw 2459	. 2 ⊢ ℘A = {x∣x ⊆ A}
4		df-pw 2459	. 2 ⊢ ℘B = {x∣x ⊆ B}
5	2, 3, 4	3eqtr4g 1574	1 ⊢ (A = B → ℘A = ℘B)

Syntax hints:   → wi 3   = wceq 992  {cab 1505   ⊆ wss 2099  ℘cpw 2458

This theorem is referenced by:  axpweq 2817  pwex 2823  pwexg 2824  pwssun 2905  canth2g 4630  pwen 4650  pwfi 4714  r1suc 4798  r1val3 4825  ranklim 4831  r1pw 4832  rankxplim 4858  mnfnre 5651  basis1 7826  eltg 7830  bastg 7834  bcth 8243  spwval2 8915  grothpw 9054  shsspwh 9394  iscomp 11114  bwt2 11123  topsinind 11136  compcov 11486  compsublem 11487  compsub 11488  uncomp 11490  hscptsscld 11491  compfipin0lem 11492  compfipin0 11493  cncomp 11494  alexsublem1 11496  alexsublem2 11497  alexsublem4 11499  alexsub 11500  is1stc 11528  2ndc1stc 11538  locfindsc 11576  topmtcl 11586  topmeet 11587  topjoin 11588  fnejoin1 11591  fgf 11632  elfg 11633  neifg 11644  isufil 11649  isufil2 11650  acdcg 11842  acdc3g 11843  acdc5g 11844  heiborlem1 12011  heiborlem9 12019  heiborlem42 12052  ishgrag 12195  hgralem 12196  ssunipwALT 12211

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-in 2103  df-ss 2105  df-pw 2459

Copyright terms: Public domain