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

Definition df-pws 14328
Description: Define a structure power, which is just a structure product where all the factors are the same. (Contributed by Mario Carneiro, 11-Jan-2015.)
Assertion
Ref Expression
df-pws
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-pws
StepHypRef Expression
1 cpws 14325 . 2
2 vr . . 3
3 vi . . 3
4 cvv 2951 . . 3
52cv 1686 . . . . 5
6 csca 14181 . . . . 5
75, 6cfv 5390 . . . 4
83cv 1686 . . . . 5
95csn 3853 . . . . 5
108, 9cxp 4809 . . . 4
11 cprds 14324 . . . 4
127, 10, 11co 6061 . . 3
132, 3, 4, 4, 12cmpt2 6063 . 2
141, 13wceq 1687 1
Colors of variables: wff setvar class
This definition is referenced by:  pwsval  14364
  Copyright terms: Public domain W3C validator