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

Definition df-cgrg 24635
 Description: Define the relation congruence bewteen shapes. Definition 4.4 of [Schwabhauser] p. 35. Ideally, we would define this for functions of any set, but we will used words (functions over ) in most cases. (Contributed by Thierry Arnoux, 3-Apr-2019.)
Assertion
Ref Expression
df-cgrg cgrG
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-cgrg
StepHypRef Expression
1 ccgrg 24634 . 2 cgrG
2 vg . . 3
3 cvv 3031 . . 3
4 va . . . . . . . 8
54cv 1451 . . . . . . 7
62cv 1451 . . . . . . . . 9
7 cbs 15199 . . . . . . . . 9
86, 7cfv 5589 . . . . . . . 8
9 cr 9556 . . . . . . . 8
10 cpm 7491 . . . . . . . 8
118, 9, 10co 6308 . . . . . . 7
125, 11wcel 1904 . . . . . 6
13 vb . . . . . . . 8
1413cv 1451 . . . . . . 7
1514, 11wcel 1904 . . . . . 6
1612, 15wa 376 . . . . 5
175cdm 4839 . . . . . . 7
1814cdm 4839 . . . . . . 7
1917, 18wceq 1452 . . . . . 6
20 vi . . . . . . . . . . . 12
2120cv 1451 . . . . . . . . . . 11
2221, 5cfv 5589 . . . . . . . . . 10
23 vj . . . . . . . . . . . 12
2423cv 1451 . . . . . . . . . . 11
2524, 5cfv 5589 . . . . . . . . . 10
26 cds 15277 . . . . . . . . . . 11
276, 26cfv 5589 . . . . . . . . . 10
2822, 25, 27co 6308 . . . . . . . . 9
2921, 14cfv 5589 . . . . . . . . . 10
3024, 14cfv 5589 . . . . . . . . . 10
3129, 30, 27co 6308 . . . . . . . . 9
3228, 31wceq 1452 . . . . . . . 8
3332, 23, 17wral 2756 . . . . . . 7
3433, 20, 17wral 2756 . . . . . 6
3519, 34wa 376 . . . . 5
3616, 35wa 376 . . . 4
3736, 4, 13copab 4453 . . 3
382, 3, 37cmpt 4454 . 2
391, 38wceq 1452 1 cgrG
 Colors of variables: wff setvar class This definition is referenced by:  iscgrg  24636  ercgrg  24641
 Copyright terms: Public domain W3C validator