Theorem pweqi 4016

Description: Equality inference for power class. (Contributed by NM, 27-Nov-2013.)

Hypothesis

Ref	Expression
pweqi.1

Assertion

Ref	Expression
pweqi

Proof of Theorem pweqi

Step	Hyp	Ref	Expression
1		pweqi.1	. 2
2		pweq 4015	. 2
3	1, 2	ax-mp 5	1

Syntax hints:  =wceq 1395  ~Pcpw 4012

This theorem is referenced by:  pwfi  7835  rankxplim  8318  pwcda1  8595  fin23lem17  8739  mnfnre  9657  qtopres  20199  hmphdis  20297  ust0  20722  shsspwh  26164  circtopn  27840  rankeq1o  29828  onsucsuccmpi  29908  elrfi  30626  islmodfg  31015  uhgrepe  32378  lcoop  33012  lincvalsc0  33022  linc0scn0  33024  lincdifsn  33025  linc1  33026  lspsslco  33038  lincresunit3lem2  33081  lincresunit3  33082

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