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

Metamath Proof Explorer

Theorem edgfndxid

Description: The value of the edge function extractor is the value of the corresponding slot of the structure. (Contributed by AV, 21-Sep-2020) (Proof shortened by AV, 28-Oct-2024)

		Ref	Expression
	Assertion	edgfndxid	⊢ ( 𝐺 ∈ 𝑉 → ( .ef ‘ 𝐺 ) = ( 𝐺 ‘ ( .ef ‘ ndx ) ) )

Proof

Step	Hyp	Ref	Expression
1		edgfid	⊢ .ef = Slot ( .ef ‘ ndx )
2		id	⊢ ( 𝐺 ∈ 𝑉 → 𝐺 ∈ 𝑉 )
3	1 2	strfvnd	⊢ ( 𝐺 ∈ 𝑉 → ( .ef ‘ 𝐺 ) = ( 𝐺 ‘ ( .ef ‘ ndx ) ) )