This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem grpidcld

Description: The identity element of a group belongs to the group. (Contributed by Thierry Arnoux, 4-May-2026)

Ref Expression
Hypotheses grpidcld.1 ⊢ B = Base G
grpidcld.2 ⊢ 0 ˙ = 0 G
grpidcld.3 ⊢ φ → G ∈ Grp
Assertion grpidcld ⊢ φ → 0 ˙ ∈ B

Proof

Step Hyp Ref Expression
1 grpidcld.1 ⊢ B = Base G
2 grpidcld.2 ⊢ 0 ˙ = 0 G
3 grpidcld.3 ⊢ φ → G ∈ Grp
4 1 2 grpidcl ⊢ G ∈ Grp → 0 ˙ ∈ B
5 3 4 syl ⊢ φ → 0 ˙ ∈ B