Metamath Proof Explorer

Definition df-eqlg

Description: Define the class of equilateral triangles. (Contributed by Thierry Arnoux, 27-Nov-2019)

Ref Expression
Assertion df-eqlg ⊢ Equilaterals 𝒢 = g ∈ V ⟼ x ∈ Base g 0 ..^ 3 | x ∼ 𝒢 ⁡ g ⟨“ x ⁡ 1 x ⁡ 2 x ⁡ 0 ”⟩

Detailed syntax breakdown

Step Hyp Ref Expression
0 ceqlg class Equilaterals 𝒢
1 vg setvar g
2 cvv class V
3 vx setvar x
4 cbs class Base
5 1 cv setvar g
6 5 4 cfv class Base g
7 cmap class ↑ 𝑚
8 cc0 class 0
9 cfzo class ..^
10 c3 class 3
11 8 10 9 co class 0 ..^ 3
12 6 11 7 co class Base g 0 ..^ 3
13 3 cv setvar x
14 ccgrg class ∼ 𝒢
15 5 14 cfv class ∼ 𝒢 ⁡ g
16 c1 class 1
17 16 13 cfv class x ⁡ 1
18 c2 class 2
19 18 13 cfv class x ⁡ 2
20 8 13 cfv class x ⁡ 0
21 17 19 20 cs3 class ⟨“ x ⁡ 1 x ⁡ 2 x ⁡ 0 ”⟩
22 13 21 15 wbr wff x ∼ 𝒢 ⁡ g ⟨“ x ⁡ 1 x ⁡ 2 x ⁡ 0 ”⟩
23 22 3 12 crab class x ∈ Base g 0 ..^ 3 | x ∼ 𝒢 ⁡ g ⟨“ x ⁡ 1 x ⁡ 2 x ⁡ 0 ”⟩
24 1 2 23 cmpt class g ∈ V ⟼ x ∈ Base g 0 ..^ 3 | x ∼ 𝒢 ⁡ g ⟨“ x ⁡ 1 x ⁡ 2 x ⁡ 0 ”⟩
25 0 24 wceq wff Equilaterals 𝒢 = g ∈ V ⟼ x ∈ Base g 0 ..^ 3 | x ∼ 𝒢 ⁡ g ⟨“ x ⁡ 1 x ⁡ 2 x ⁡ 0 ”⟩