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

Theorem pweqd 4017
Description: Equality deduction for power class. (Contributed by NM, 27-Nov-2013.)
Hypothesis
Ref Expression
pweqd.1
Assertion
Ref Expression
pweqd

Proof of Theorem pweqd
StepHypRef Expression
1 pweqd.1 . 2
2 pweq 4015 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  ~Pcpw 4012
This theorem is referenced by:  undefval  7024  pmvalg  7450  marypha1lem  7913  marypha1  7914  r1val3  8277  ackbij1lem5  8625  ackbij2lem2  8641  ackbij2lem3  8642  r1om  8645  isfin2  8695  hsmexlem8  8825  vdwmc  14496  hashbcval  14520  ismre  14987  mrcfval  15005  mrisval  15027  mreexexlemd  15041  brssc  15183  lubfval  15608  glbfval  15621  isclat  15739  issubm  15978  issubg  16201  cntzfval  16358  symgval  16404  lsmfval  16658  lsmpropd  16695  pj1fval  16712  issubrg  17429  lssset  17580  lspfval  17619  lsppropd  17664  islbs  17722  sraval  17822  aspval  17977  opsrval  18139  ply1frcl  18355  evls1fval  18356  ocvfval  18697  isobs  18751  islinds  18844  basis1  19451  baspartn  19455  cldval  19524  ntrfval  19525  clsfval  19526  mretopd  19593  neifval  19600  lpfval  19639  cncls2  19774  iscnrm  19824  iscnrm2  19839  2ndcsep  19960  kgenval  20036  xkoval  20088  dfac14  20119  qtopval  20196  qtopval2  20197  isfbas  20330  trfbas2  20344  flimval  20464  elflim  20472  flimclslem  20485  fclsfnflim  20528  fclscmp  20531  tsmsfbas  20626  tsmsval2  20628  ustval  20705  utopval  20735  mopnfss  20946  setsmstopn  20981  met2ndc  21026  istrkgb  23852  isumgra  24315  isuslgra  24343  isusgra  24344  edgss  24352  ismeas  28170  omsval  28264  oms0  28266  omsmon  28267  erdszelem3  28637  erdsze  28646  kur14  28660  iscvm  28704  mpstval  28895  mclsval  28923  heibor  30317  idlval  30410  igenval  30458  mzpclval  30657  dfac21  31012  islmodfg  31015  islssfg  31016  rgspnval  31117  isuhgr  32366  isushgr  32367  uhgun  32380  issubmgm  32477  lincop  33009  lcoop  33012  islininds  33047  ldepsnlinc  33109  paddfval  35521  pclfvalN  35613  polfvalN  35628  docaffvalN  36848  docafvalN  36849  djaffvalN  36860  djafvalN  36861  dochffval  37076  dochfval  37077  djhffval  37123  djhfval  37124  lpolsetN  37209  lcdlss2N  37347
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