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

Definition df-struct 14168
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
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-struct
StepHypRef Expression
1 cstr 14162 . 2
2 vx . . . . . 6
32cv 1368 . . . . 5
4 cle 9411 . . . . . 6
5 cn 10314 . . . . . . 7
65, 5cxp 4833 . . . . . 6
74, 6cin 3322 . . . . 5
83, 7wcel 1756 . . . 4
9 vf . . . . . . 7
109cv 1368 . . . . . 6
11 c0 3632 . . . . . . 7
1211csn 3872 . . . . . 6
1310, 12cdif 3320 . . . . 5
1413wfun 5407 . . . 4
1510cdm 4835 . . . . 5
16 cfz 11429 . . . . . 6
173, 16cfv 5413 . . . . 5
1815, 17wss 3323 . . . 4
198, 14, 18w3a 965 . . 3
2019, 9, 2copab 4344 . 2
211, 20wceq 1369 1
Colors of variables: wff setvar class
This definition is referenced by:  brstruct  14174  isstruct2  14175
  Copyright terms: Public domain W3C validator