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=SlotI
Assertion str0 =F

Proof

Step Hyp Ref Expression
1 str0.a F=SlotI
2 0ex V
3 2 1 strfvn F=I
4 0fv I=
5 3 4 eqtr2i =F