df-cgr - Metamath Proof Explorer

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

Definition df-cgr 25773

Description: Define the Euclidean congruence predicate. For details, see brcgr 25780. (Contributed by Scott Fenton, 3-Jun-2013.)

**Assertion**
Ref	Expression
df-cgr	Cgr $/\$ $/\$

**Detailed syntax breakdown of Definition df-cgr**
Step	Hyp	Ref	Expression
1		ccgr 25770	. 2 Cgr
2		vx	. . . . . . . 8
3	2	cv 1482	. . . . . . 7
4		vn	. . . . . . . . . 10
5	4	cv 1482	. . . . . . . . 9
6		cee 25768	. . . . . . . . 9
7	5, 6	cfv 5888	. . . . . . . 8
8	7, 7	cxp 5112	. . . . . . 7
9	3, 8	wcel 1990	. . . . . 6
10		vy	. . . . . . . 8
11	10	cv 1482	. . . . . . 7
12	11, 8	wcel 1990	. . . . . 6
13	9, 12	wa 384	. . . . 5 $/\$
14		c1 9937	. . . . . . . 8
15		cfz 12326	. . . . . . . 8
16	14, 5, 15	co 6650	. . . . . . 7
17		vi	. . . . . . . . . . 11
18	17	cv 1482	. . . . . . . . . 10
19		c1st 7166	. . . . . . . . . . 11
20	3, 19	cfv 5888	. . . . . . . . . 10
21	18, 20	cfv 5888	. . . . . . . . 9
22		c2nd 7167	. . . . . . . . . . 11
23	3, 22	cfv 5888	. . . . . . . . . 10
24	18, 23	cfv 5888	. . . . . . . . 9
25		cmin 10266	. . . . . . . . 9
26	21, 24, 25	co 6650	. . . . . . . 8
27		c2 11070	. . . . . . . 8
28		cexp 12860	. . . . . . . 8
29	26, 27, 28	co 6650	. . . . . . 7
30	16, 29, 17	csu 14416	. . . . . 6
31	11, 19	cfv 5888	. . . . . . . . . 10
32	18, 31	cfv 5888	. . . . . . . . 9
33	11, 22	cfv 5888	. . . . . . . . . 10
34	18, 33	cfv 5888	. . . . . . . . 9
35	32, 34, 25	co 6650	. . . . . . . 8
36	35, 27, 28	co 6650	. . . . . . 7
37	16, 36, 17	csu 14416	. . . . . 6
38	30, 37	wceq 1483	. . . . 5
39	13, 38	wa 384	. . . 4 $/\$ $/\$
40		cn 11020	. . . 4
41	39, 4, 40	wrex 2913	. . 3 $/\$ $/\$
42	41, 2, 10	copab 4712	. 2 $/\$ $/\$
43	1, 42	wceq 1483	1 Cgr $/\$ $/\$

Colors of variables: wff setvar class

This definition is referenced by: brcgr 25780