# 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}_{𝒢}=\left({g}\in \mathrm{V}⟼\left\{{x}\in \left({{\mathrm{Base}}_{{g}}}^{\left(0..^3\right)}\right)|{x}{\sim }_{𝒢}\left({g}\right)⟨“{x}\left(1\right){x}\left(2\right){x}\left(0\right)”⟩\right\}\right)$

### Detailed syntax breakdown

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