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	⊢ 𝐸 = Slot 𝑁
Assertion	strfvss	⊢ ( 𝐸 ‘ 𝑆 ) ⊆ ∪ ran 𝑆

Proof

Step	Hyp	Ref	Expression
1		strfvss.e	⊢ 𝐸 = Slot 𝑁
2		id	⊢ ( 𝑆 ∈ V → 𝑆 ∈ V )
3	1 2	strfvnd	⊢ ( 𝑆 ∈ V → ( 𝐸 ‘ 𝑆 ) = ( 𝑆 ‘ 𝑁 ) )
4		fvssunirn	⊢ ( 𝑆 ‘ 𝑁 ) ⊆ ∪ ran 𝑆
5	3 4	eqsstrdi	⊢ ( 𝑆 ∈ V → ( 𝐸 ‘ 𝑆 ) ⊆ ∪ ran 𝑆 )
6		fvprc	⊢ ( ¬ 𝑆 ∈ V → ( 𝐸 ‘ 𝑆 ) = ∅ )
7		0ss	⊢ ∅ ⊆ ∪ ran 𝑆
8	6 7	eqsstrdi	⊢ ( ¬ 𝑆 ∈ V → ( 𝐸 ‘ 𝑆 ) ⊆ ∪ ran 𝑆 )
9	5 8	pm2.61i	⊢ ( 𝐸 ‘ 𝑆 ) ⊆ ∪ ran 𝑆