Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > dfsets  Unicode version 
Description: Set one or more components of a structure. This function is useful for taking an existing structure and "overriding" one of its components. For example, dfress 13431 adjusts the base set to match its second argument, which has the effect of making subgroups, subspaces, subrings etc. from the original structures. Or dfmgp 15604, which takes a ring and overrides its addition operation with the multiplicative operation, so that we can consider the "multiplicative group" using group and monoid theorems, which expect the operation to be in the slot instead of the slot. (Contributed by Mario Carneiro, 1Dec2014.) 
Ref  Expression 

dfsets  sSet 
Step  Hyp  Ref  Expression 

1  csts 13422  . 2 sSet  
2  vs  . . 3  
3  ve  . . 3  
4  cvv 2916  . . 3  
5  2  cv 1648  . . . . 5 
6  3  cv 1648  . . . . . . . 8 
7  6  csn 3774  . . . . . . 7 
8  7  cdm 4837  . . . . . 6 
9  4, 8  cdif 3277  . . . . 5 
10  5, 9  cres 4839  . . . 4 
11  10, 7  cun 3278  . . 3 
12  2, 3, 4, 4, 11  cmpt2 6042  . 2 
13  1, 12  wceq 1649  1 sSet 
Colors of variables: wff set class 
This definition is referenced by: reldmsets 13446 setsvalg 13447 
Copyright terms: Public domain  W3C validator 