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 a fixed integer such as 1 . S is a structure, i.e. a specific member of a class of structures such as Poset ( df-poset ) where S e. Poset .

Note: Normally, this theorem shouldn't be used outside of this section, because it requires hard-coded index values. Instead, use strfv . (Contributed by NM, 9-Sep-2011) (Revised by Mario Carneiro, 6-Oct-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	strfvn.f	$$⊢S\in \mathrm{V}$$
	strfvn.c	$$⊢E=\mathrm{Slot}N$$
Assertion	strfvn	$$⊢E\left(S\right)=S\left(N\right)$$

Proof

Step	Hyp	Ref	Expression
1		strfvn.f	$$⊢S\in \mathrm{V}$$
2		strfvn.c	$$⊢E=\mathrm{Slot}N$$
3	1	a1i	$$⊢\top \to S\in \mathrm{V}$$
4	2 3	strfvnd	$$⊢\top \to E\left(S\right)=S\left(N\right)$$
5	4	mptru	$$⊢E\left(S\right)=S\left(N\right)$$