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

Definition df-struct 13476
 Description: Define a structure with components in . This is not a requirement for groups, posets, etc., but it is a useful assumption for component extraction theorems. (Contributed by Mario Carneiro, 29-Aug-2015.)
Assertion
Ref Expression
df-struct Struct
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-struct
StepHypRef Expression
1 cstr 13470 . 2 Struct
2 vx . . . . . 6
32cv 1652 . . . . 5
4 cle 9126 . . . . . 6
5 cn 10005 . . . . . . 7
65, 5cxp 4879 . . . . . 6
74, 6cin 3321 . . . . 5
83, 7wcel 1726 . . . 4
9 vf . . . . . . 7
109cv 1652 . . . . . 6
11 c0 3630 . . . . . . 7
1211csn 3816 . . . . . 6
1310, 12cdif 3319 . . . . 5
1413wfun 5451 . . . 4
1510cdm 4881 . . . . 5
16 cfz 11048 . . . . . 6
173, 16cfv 5457 . . . . 5
1815, 17wss 3322 . . . 4
198, 14, 18w3a 937 . . 3
2019, 9, 2copab 4268 . 2
211, 20wceq 1653 1 Struct
 Colors of variables: wff set class This definition is referenced by:  brstruct  13482  isstruct2  13483
 Copyright terms: Public domain W3C validator