Database
BASIC STRUCTURES
Extensible structures
Slot definitions
plusgid
Next ⟩
opelstrbas
Metamath Proof Explorer
Ascii
Unicode
Theorem
plusgid
Description:
Utility theorem: index-independent form of
df-plusg
.
(Contributed by
NM
, 20-Oct-2012)
Ref
Expression
Assertion
plusgid
⊢
+
𝑔
=
Slot
+
ndx
Proof
Step
Hyp
Ref
Expression
1
df-plusg
⊢
+
𝑔
=
Slot
2
2
2nn
⊢
2
∈
ℕ
3
1
2
ndxid
⊢
+
𝑔
=
Slot
+
ndx