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

Metamath Proof Explorer

Theorem ringidcld

Description: The unity element of a ring belongs to the base set of the ring, deduction version. (Contributed by SN, 16-Oct-2025)

Ref Expression
Hypotheses ringidcl.b ⊢ B = Base R
ringidcl.u ⊢ 1 ˙ = 1 R
ringidcld.r ⊢ φ → R ∈ Ring
Assertion ringidcld ⊢ φ → 1 ˙ ∈ B

Proof

Step Hyp Ref Expression
1 ringidcl.b ⊢ B = Base R
2 ringidcl.u ⊢ 1 ˙ = 1 R
3 ringidcld.r ⊢ φ → R ∈ Ring
4 1 2 ringidcl ⊢ R ∈ Ring → 1 ˙ ∈ B
5 3 4 syl ⊢ φ → 1 ˙ ∈ B