Mathbox for Frédéric Liné < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-cst Unicode version

Definition df-cst 25173
 Description: Define an operation on the subsets derived from an operation on the elements. Meaningful if is a binary internal operation. (Contributed by FL, 18-Apr-2010.)
Assertion
Ref Expression
df-cst
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-cst
StepHypRef Expression
1 ccst 25172 . 2
2 vg . . 3
3 cvv 2788 . . 3
4 vx . . . 4
5 vy . . . 4
62cv 1622 . . . . . . 7
76cdm 4689 . . . . . 6
87cdm 4689 . . . . 5
98cpw 3625 . . . 4
10 vu . . . . . 6
11 vv . . . . . 6
124cv 1622 . . . . . 6
135cv 1622 . . . . . 6
1410cv 1622 . . . . . . 7
1511cv 1622 . . . . . . 7
1614, 15, 6co 5858 . . . . . 6
1710, 11, 12, 13, 16cmpt2 5860 . . . . 5
1817crn 4690 . . . 4
194, 5, 9, 9, 18cmpt2 5860 . . 3
202, 3, 19cmpt 4077 . 2
211, 20wceq 1623 1
 Colors of variables: wff set class This definition is referenced by:  iscst1  25174
 Copyright terms: Public domain W3C validator