Description: A structure component extractor produces a value which is contained in a set dependent on S , but not E . This is sometimes useful for showing sethood. (Contributed by Mario Carneiro, 15-Aug-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | strfvss.e | |- E = Slot N |
|
| Assertion | strfvss | |- ( E ` S ) C_ U. ran S |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | strfvss.e | |- E = Slot N |
|
| 2 | id | |- ( S e. _V -> S e. _V ) |
|
| 3 | 1 2 | strfvnd | |- ( S e. _V -> ( E ` S ) = ( S ` N ) ) |
| 4 | fvssunirn | |- ( S ` N ) C_ U. ran S |
|
| 5 | 3 4 | eqsstrdi | |- ( S e. _V -> ( E ` S ) C_ U. ran S ) |
| 6 | fvprc | |- ( -. S e. _V -> ( E ` S ) = (/) ) |
|
| 7 | 0ss | |- (/) C_ U. ran S |
|
| 8 | 6 7 | eqsstrdi | |- ( -. S e. _V -> ( E ` S ) C_ U. ran S ) |
| 9 | 5 8 | pm2.61i | |- ( E ` S ) C_ U. ran S |