# Metamath Proof Explorer

## Theorem strfvss

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 ndxarg.1 ${⊢}{E}=\mathrm{Slot}{N}$
Assertion strfvss ${⊢}{E}\left({S}\right)\subseteq \bigcup \mathrm{ran}{S}$

### Proof

Step Hyp Ref Expression
1 ndxarg.1 ${⊢}{E}=\mathrm{Slot}{N}$
2 id ${⊢}{S}\in \mathrm{V}\to {S}\in \mathrm{V}$
3 1 2 strfvnd ${⊢}{S}\in \mathrm{V}\to {E}\left({S}\right)={S}\left({N}\right)$
4 fvssunirn ${⊢}{S}\left({N}\right)\subseteq \bigcup \mathrm{ran}{S}$
5 3 4 eqsstrdi ${⊢}{S}\in \mathrm{V}\to {E}\left({S}\right)\subseteq \bigcup \mathrm{ran}{S}$
6 fvprc ${⊢}¬{S}\in \mathrm{V}\to {E}\left({S}\right)=\varnothing$
7 0ss ${⊢}\varnothing \subseteq \bigcup \mathrm{ran}{S}$
8 6 7 eqsstrdi ${⊢}¬{S}\in \mathrm{V}\to {E}\left({S}\right)\subseteq \bigcup \mathrm{ran}{S}$
9 5 8 pm2.61i ${⊢}{E}\left({S}\right)\subseteq \bigcup \mathrm{ran}{S}$