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

Definition df-struct 13426
 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 13420 . 2 Struct
2 vx . . . . . 6
32cv 1648 . . . . 5
4 cle 9077 . . . . . 6
5 cn 9956 . . . . . . 7
65, 5cxp 4835 . . . . . 6
74, 6cin 3279 . . . . 5
83, 7wcel 1721 . . . 4
9 vf . . . . . . 7
109cv 1648 . . . . . 6
11 c0 3588 . . . . . . 7
1211csn 3774 . . . . . 6
1310, 12cdif 3277 . . . . 5
1413wfun 5407 . . . 4
1510cdm 4837 . . . . 5
16 cfz 10999 . . . . . 6
173, 16cfv 5413 . . . . 5
1815, 17wss 3280 . . . 4
198, 14, 18w3a 936 . . 3
2019, 9, 2copab 4225 . 2
211, 20wceq 1649 1 Struct
 Colors of variables: wff set class This definition is referenced by:  brstruct  13432  isstruct2  13433
 Copyright terms: Public domain W3C validator