This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ∅ ∈ V
3 2 1 strfvn ⊢ F ⁡ ∅ = ∅ ⁡ I
4 0fv ⊢ ∅ ⁡ I = ∅
5 3 4 eqtr2i ⊢ ∅ = F ⁡ ∅