Description: The value of a structure component extractor is the value of the corresponding slot of the structure. (Contributed by AV, 13-Mar-2020) (New usage is discouraged.) Use strfvnd directly with N set to ( Endx ) if possible.
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | strndxid.s | |- ( ph -> S e. V ) |
|
| strndxid.e | |- E = Slot N |
||
| strndxid.n | |- N e. NN |
||
| Assertion | strndxid | |- ( ph -> ( S ` ( E ` ndx ) ) = ( E ` S ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | strndxid.s | |- ( ph -> S e. V ) |
|
| 2 | strndxid.e | |- E = Slot N |
|
| 3 | strndxid.n | |- N e. NN |
|
| 4 | 2 3 | ndxid | |- E = Slot ( E ` ndx ) |
| 5 | 4 1 | strfvnd | |- ( ph -> ( E ` S ) = ( S ` ( E ` ndx ) ) ) |
| 6 | 5 | eqcomd | |- ( ph -> ( S ` ( E ` ndx ) ) = ( E ` S ) ) |