Mathbox for Frédéric Liné < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-trcng Unicode version

Definition df-trcng 25542
 Description: Congruence of two triangles. Triangles are congruent if their sides and angles are congruent. "Technically, congruence is not a property of triangles themselves, but of triangles with a given ordering of their vertices. Triangles that are congruent under one ordering, might not be under other orderings." Definition 2 of [AitkenIBCG] p. 3. (Contributed by FL, 2-Sep-2016.)
Assertion
Ref Expression
df-trcng trcng PPointsdWords PPointsdWords segtrgsegcsegtrg segtrgsegcsegtrg segtrgsegcsegtrg angtrgangcangtrg angtrgangcangtrg angtrgangcangtrg
Distinct variable group:   ,,

Detailed syntax breakdown of Definition df-trcng
StepHypRef Expression
1 ctrcng 25514 . 2 trcng
2 vg . . 3
3 cvv 2757 . . 3
4 vu . . . . . . . 8
54cv 1618 . . . . . . 7
62cv 1618 . . . . . . . . 9
7 cpoints 25409 . . . . . . . . 9 PPoints
86, 7cfv 4659 . . . . . . . 8 PPoints
9 c3 9750 . . . . . . . 8
10 cdwords 25337 . . . . . . . 8 dWords
118, 9, 10co 5778 . . . . . . 7 PPointsdWords
125, 11wcel 1621 . . . . . 6 PPointsdWords
13 vv . . . . . . . 8
1413cv 1618 . . . . . . 7
1514, 11wcel 1621 . . . . . 6 PPointsdWords
1612, 15wa 360 . . . . 5 PPointsdWords PPointsdWords
17 c1 8692 . . . . . . . 8
18 csegtrg 25540 . . . . . . . . 9 segtrg
196, 18cfv 4659 . . . . . . . 8 segtrg
205, 17, 19co 5778 . . . . . . 7 segtrg
2114, 17, 19co 5778 . . . . . . 7 segtrg
22 csegc 25533 . . . . . . . 8 segc
236, 22cfv 4659 . . . . . . 7 segc
2420, 21, 23wbr 3983 . . . . . 6 segtrgsegcsegtrg
25 c2 9749 . . . . . . . 8
265, 25, 19co 5778 . . . . . . 7 segtrg
2714, 25, 19co 5778 . . . . . . 7 segtrg
2826, 27, 23wbr 3983 . . . . . 6 segtrgsegcsegtrg
295, 9, 19co 5778 . . . . . . 7 segtrg
3014, 9, 19co 5778 . . . . . . 7 segtrg
3129, 30, 23wbr 3983 . . . . . 6 segtrgsegcsegtrg
3224, 28, 31w3a 939 . . . . 5 segtrgsegcsegtrg segtrgsegcsegtrg segtrgsegcsegtrg
33 cangtrg 25538 . . . . . . . . 9 angtrg
346, 33cfv 4659 . . . . . . . 8 angtrg
355, 25, 34co 5778 . . . . . . 7 angtrg
3614, 25, 34co 5778 . . . . . . 7 angtrg
37 cangc 25536 . . . . . . . 8 angc
386, 37cfv 4659 . . . . . . 7 angc
3935, 36, 38wbr 3983 . . . . . 6 angtrgangcangtrg
405, 9, 34co 5778 . . . . . . 7 angtrg
4114, 9, 34co 5778 . . . . . . 7 angtrg
4240, 41, 38wbr 3983 . . . . . 6 angtrgangcangtrg
435, 17, 34co 5778 . . . . . . 7 angtrg
4414, 17, 34co 5778 . . . . . . 7 angtrg
4543, 44, 38wbr 3983 . . . . . 6 angtrgangcangtrg
4639, 42, 45w3a 939 . . . . 5 angtrgangcangtrg angtrgangcangtrg angtrgangcangtrg
4716, 32, 46w3a 939 . . . 4 PPointsdWords PPointsdWords segtrgsegcsegtrg segtrgsegcsegtrg segtrgsegcsegtrg angtrgangcangtrg angtrgangcangtrg angtrgangcangtrg
4847, 4, 13copab 4036 . . 3 PPointsdWords PPointsdWords segtrgsegcsegtrg segtrgsegcsegtrg segtrgsegcsegtrg angtrgangcangtrg angtrgangcangtrg angtrgangcangtrg
492, 3, 48cmpt 4037 . 2 PPointsdWords PPointsdWords segtrgsegcsegtrg segtrgsegcsegtrg segtrgsegcsegtrg angtrgangcangtrg angtrgangcangtrg angtrgangcangtrg
501, 49wceq 1619 1 trcng PPointsdWords PPointsdWords segtrgsegcsegtrg segtrgsegcsegtrg segtrgsegcsegtrg angtrgangcangtrg angtrgangcangtrg angtrgangcangtrg
 Colors of variables: wff set class
 Copyright terms: Public domain W3C validator