Metamath Proof Explorer

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 = Slot I
Assertion str0 
|- (/) = ( F ` (/) )

Proof

Step Hyp Ref Expression
1 str0.a 
 |-  F = Slot I
2 0ex 
 |-  (/) e. _V
3 2 1 strfvn 
 |-  ( F ` (/) ) = ( (/) ` I )
4 0fv 
 |-  ( (/) ` I ) = (/)
5 3 4 eqtr2i 
 |-  (/) = ( F ` (/) )