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 | |- S e. _V |
|
| strfvn.c | |- E = Slot N |
||
| Assertion | strfvn | |- ( E ` S ) = ( S ` N ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | strfvn.f | |- S e. _V |
|
| 2 | strfvn.c | |- E = Slot N |
|
| 3 | 1 | a1i | |- ( T. -> S e. _V ) |
| 4 | 2 3 | strfvnd | |- ( T. -> ( E ` S ) = ( S ` N ) ) |
| 5 | 4 | mptru | |- ( E ` S ) = ( S ` N ) |