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

Definition df-scaf 15945
 Description: Define the functionalization of the operator. This restricts the value of to the stated domain, which is necessary when working with restricted structures, whose operations may be defined on a larger set than the true base. (Contributed by Mario Carneiro, 5-Oct-2015.)
Assertion
Ref Expression
df-scaf Scalar
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-scaf
StepHypRef Expression
1 cscaf 15943 . 2
2 vg . . 3
3 cvv 2948 . . 3
4 vx . . . 4
5 vy . . . 4
62cv 1651 . . . . . 6
7 csca 13524 . . . . . 6 Scalar
86, 7cfv 5446 . . . . 5 Scalar
9 cbs 13461 . . . . 5
108, 9cfv 5446 . . . 4 Scalar
116, 9cfv 5446 . . . 4
124cv 1651 . . . . 5
135cv 1651 . . . . 5
14 cvsca 13525 . . . . . 6
156, 14cfv 5446 . . . . 5
1612, 13, 15co 6073 . . . 4
174, 5, 10, 11, 16cmpt2 6075 . . 3 Scalar
182, 3, 17cmpt 4258 . 2 Scalar
191, 18wceq 1652 1 Scalar
 Colors of variables: wff set class This definition is referenced by:  scaffval  15960
 Copyright terms: Public domain W3C validator