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

Metamath Proof Explorer

Theorem supp0

Description: The support of the empty set is the empty set. (Contributed by AV, 12-Apr-2019)

Ref Expression
Assertion supp0 ⊢ Z ∈ W → ∅ supp Z = ∅

Proof

Step Hyp Ref Expression
1 0ex ⊢ ∅ ∈ V
2 suppval ⊢ ∅ ∈ V ∧ Z ∈ W → ∅ supp Z = i ∈ dom ⁡ ∅ | ∅ i ≠ Z
3 1 2 mpan ⊢ Z ∈ W → ∅ supp Z = i ∈ dom ⁡ ∅ | ∅ i ≠ Z
4 dm0 ⊢ dom ⁡ ∅ = ∅
5 rabeq ⊢ dom ⁡ ∅ = ∅ → i ∈ dom ⁡ ∅ | ∅ i ≠ Z = i ∈ ∅ | ∅ i ≠ Z
6 4 5 mp1i ⊢ Z ∈ W → i ∈ dom ⁡ ∅ | ∅ i ≠ Z = i ∈ ∅ | ∅ i ≠ Z
7 rab0 ⊢ i ∈ ∅ | ∅ i ≠ Z = ∅
8 7 a1i ⊢ Z ∈ W → i ∈ ∅ | ∅ i ≠ Z = ∅
9 3 6 8 3eqtrd ⊢ Z ∈ W → ∅ supp Z = ∅