MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pweq Unicode version

Theorem pweq 4015
Description: Equality theorem for power class. (Contributed by NM, 21-Jun-1993.)
Assertion
Ref Expression
pweq

Proof of Theorem pweq
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 sseq2 3525 . . 3
21abbidv 2593 . 2
3 df-pw 4014 . 2
4 df-pw 4014 . 2
52, 3, 43eqtr4g 2523 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  {cab 2442  C_wss 3475  ~Pcpw 4012
This theorem is referenced by:  pweqi  4016  pweqd  4017  axpweq  4629  pwex  4635  pwexg  4636  pwssun  4791  knatar  6253  pwdom  7689  canth2g  7691  pwfi  7835  fival  7892  marypha1lem  7913  marypha1  7914  wdompwdom  8025  canthwdom  8026  r1sucg  8208  ranklim  8283  r1pwOLD  8285  isacn  8446  dfac12r  8547  dfac12k  8548  pwsdompw  8605  ackbij1lem5  8625  ackbij1lem8  8628  ackbij1lem14  8634  r1om  8645  fictb  8646  isfin1a  8693  isfin2  8695  isfin3  8697  isfin3ds  8730  isf33lem  8767  domtriomlem  8843  ttukeylem1  8910  elgch  9021  wunpw  9106  wunex2  9137  wuncval2  9146  eltskg  9149  eltsk2g  9150  tskpwss  9151  tskpw  9152  inar1  9174  grupw  9194  grothpw  9225  grothpwex  9226  axgroth6  9227  grothomex  9228  grothac  9229  axdc4uz  12093  hashpw  12494  hashbc  12502  ackbijnn  13640  incexclem  13648  rami  14533  ismre  14987  isacs  15048  isacs2  15050  acsfiel  15051  isacs1i  15054  mreacs  15055  isssc  15189  acsficl  15801  pmtrfval  16475  istopg  19404  istopon  19426  eltg  19458  tgdom  19480  ntrval  19537  nrmsep3  19856  iscmp  19888  cmpcov  19889  cmpsublem  19899  cmpsub  19900  tgcmp  19901  uncmp  19903  hauscmplem  19906  bwthOLD  19911  is1stc  19942  2ndc1stc  19952  llyi  19975  nllyi  19976  cldllycmp  19996  isfbas  20330  isfil  20348  filss  20354  fgval  20371  elfg  20372  isufil  20404  alexsublem  20544  alexsubb  20546  alexsubALTlem1  20547  alexsubALTlem2  20548  alexsubALTlem4  20550  alexsubALT  20551  restmetu  21090  bndth  21458  ovolicc2  21933  isuhgra  24298  isushgra  24301  uhgrac  24305  uhgraeq12d  24307  isausgra  24354  usgraeq12d  24362  ex-pw  25150  issubgo  25305  iscref  27847  indv  28026  sigaval  28110  issiga  28111  isrnsigaOLD  28112  isrnsiga  28113  issgon  28123  measval  28169  isrnmeas  28171  rankpwg  29826  limsucncmpi  29910  neibastop1  30177  neibastop2lem  30178  neibastop2  30179  neibastop3  30180  neifg  30189  cover2g  30205  isnacs  30636  mrefg2  30639  aomclem8  31007  islssfg2  31017  lnr2i  31065  stoweidlem50  31832  stoweidlem57  31839  uhgeq12g  32370  uhguhgra  32372  uhgrauhg  32373  uhg0v  32377  isfusgra  32424  bj-snglex  34531  pwelg  37745
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489  df-pw 4014
  Copyright terms: Public domain W3C validator