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

Proof

Step	Hyp	Ref	Expression
1		strfvss.e	$$⊢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	$$⊢\neg S\in \mathrm{V}\to E\left(S\right)=\varnothing$$
7		0ss	$$⊢\varnothing \subseteq \bigcup \mathrm{ran}S$$
8	6 7	eqsstrdi	$$⊢\neg 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$$