Theorem strfvn

Description: Value of a structure component extractor E . Normally, E is a defined constant symbol such as Base ( df-base ) and N is the index of the component. S is a structure, i.e. a specific member of a class of structures such as Poset ( df-poset ) where S e. Poset .

Hint: Do not substitute N by a specific (positive) integer to be independent of a hard-coded index value. Often, ( Endx ) can be used instead of N . Alternatively, use strfv instead of strfvn . (Contributed by NM, 9-Sep-2011) (Revised by Mario Carneiro, 6-Oct-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	strfvn.f	⊢ 𝑆 ∈ V
	strfvn.c	⊢ 𝐸 = Slot 𝑁
Assertion	strfvn	⊢ ( 𝐸 ‘ 𝑆 ) = ( 𝑆 ‘ 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		strfvn.f	⊢ 𝑆 ∈ V
2		strfvn.c	⊢ 𝐸 = Slot 𝑁
3	1	a1i	⊢ ( ⊤ → 𝑆 ∈ V )
4	2 3	strfvnd	⊢ ( ⊤ → ( 𝐸 ‘ 𝑆 ) = ( 𝑆 ‘ 𝑁 ) )
5	4	mptru	⊢ ( 𝐸 ‘ 𝑆 ) = ( 𝑆 ‘ 𝑁 )