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 ⊢ 𝐵 = ( Base ‘ 𝑅 )
ringidcl.u ⊢ 1 = ( 1r ‘ 𝑅 )
ringidcld.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
Assertion ringidcld ( 𝜑 → 1 ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 ringidcl.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 ringidcl.u ⊢ 1 = ( 1r ‘ 𝑅 )
3 ringidcld.r ⊢ ( 𝜑 → 𝑅 ∈ Ring )
4 1 2 ringidcl ⊢ ( 𝑅 ∈ Ring → 1 ∈ 𝐵 )
5 3 4 syl ⊢ ( 𝜑 → 1 ∈ 𝐵 )