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	$$⊢F=\mathrm{Slot}I$$
Assertion	str0	$$⊢\varnothing =F\left(\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		str0.a	$$⊢F=\mathrm{Slot}I$$
2		0ex	$$⊢\varnothing \in \mathrm{V}$$
3	2 1	strfvn	$$⊢F\left(\varnothing \right)=\varnothing \left(I\right)$$
4		0fv	$$⊢\varnothing \left(I\right)=\varnothing$$
5	3 4	eqtr2i	$$⊢\varnothing =F\left(\varnothing \right)$$