Database
GRAPH THEORY
Vertices and edges
The edge function extractor for extensible structures
edgfid
Next ⟩
edgfndx
Metamath Proof Explorer
Ascii
Unicode
Theorem
edgfid
Description:
Utility theorem: index-independent form of
df-edgf
.
(Contributed by
AV
, 16-Nov-2021)
Ref
Expression
Assertion
edgfid
⊢
ef
=
Slot
ef
⁡
ndx
Proof
Step
Hyp
Ref
Expression
1
df-edgf
⊢
ef
=
Slot
18
2
1nn0
⊢
1
∈
ℕ
0
3
8nn
⊢
8
∈
ℕ
4
2
3
decnncl
⊢
18
∈
ℕ
5
1
4
ndxid
⊢
ef
=
Slot
ef
⁡
ndx