Metamath Proof Explorer


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 𝑆 ∈ 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 ( 𝐸𝑆 ) = ( 𝑆𝑁 )