Theorem str0

Description: All components of the empty set are empty sets. (Contributed by Stefan O'Rear, 27-Nov-2014) (Revised by Mario Carneiro, 7-Dec-2014)

	Ref	Expression
Hypothesis	str0.a	⊢ 𝐹 = Slot 𝐼
Assertion	str0	⊢ ∅ = ( 𝐹 ‘ ∅ )

Proof

Step	Hyp	Ref	Expression
1		str0.a	⊢ 𝐹 = Slot 𝐼
2		0ex	⊢ ∅ ∈ V
3	2 1	strfvn	⊢ ( 𝐹 ‘ ∅ ) = ( ∅ ‘ 𝐼 )
4		0fv	⊢ ( ∅ ‘ 𝐼 ) = ∅
5	3 4	eqtr2i	⊢ ∅ = ( 𝐹 ‘ ∅ )