Metamath Proof Explorer

Theorem strfv

Description: Extract a structure component C (such as the base set) from a structure S (such as a member of Poset , df-poset ) with a component extractor E (such as the base set extractor df-base ). By virtue of ndxid , this can be done without having to refer to the hard-coded numeric index of E . (Contributed by Mario Carneiro, 6-Oct-2013) (Revised by Mario Carneiro, 29-Aug-2015)

Ref Expression
Hypotheses strfv.s S Struct X
strfv.e E = Slot E ndx
strfv.n E ndx C S
Assertion strfv C V C = E S


Step Hyp Ref Expression
1 strfv.s S Struct X
2 strfv.e E = Slot E ndx
3 strfv.n E ndx C S
4 structex S Struct X S V
5 1 4 ax-mp S V
6 1 structfun Fun S -1 -1
7 opex E ndx C V
8 7 snss E ndx C S E ndx C S
9 3 8 mpbir E ndx C S
10 5 6 2 9 strfv2 C V C = E S