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 ( 𝑍𝑊 → ( ∅ supp 𝑍 ) = ∅ )

Proof

Step Hyp Ref Expression
1 0ex ∅ ∈ V
2 suppval ( ( ∅ ∈ V ∧ 𝑍𝑊 ) → ( ∅ supp 𝑍 ) = { 𝑖 ∈ dom ∅ ∣ ( ∅ “ { 𝑖 } ) ≠ { 𝑍 } } )
3 1 2 mpan ( 𝑍𝑊 → ( ∅ supp 𝑍 ) = { 𝑖 ∈ dom ∅ ∣ ( ∅ “ { 𝑖 } ) ≠ { 𝑍 } } )
4 dm0 dom ∅ = ∅
5 rabeq ( dom ∅ = ∅ → { 𝑖 ∈ dom ∅ ∣ ( ∅ “ { 𝑖 } ) ≠ { 𝑍 } } = { 𝑖 ∈ ∅ ∣ ( ∅ “ { 𝑖 } ) ≠ { 𝑍 } } )
6 4 5 mp1i ( 𝑍𝑊 → { 𝑖 ∈ dom ∅ ∣ ( ∅ “ { 𝑖 } ) ≠ { 𝑍 } } = { 𝑖 ∈ ∅ ∣ ( ∅ “ { 𝑖 } ) ≠ { 𝑍 } } )
7 rab0 { 𝑖 ∈ ∅ ∣ ( ∅ “ { 𝑖 } ) ≠ { 𝑍 } } = ∅
8 7 a1i ( 𝑍𝑊 → { 𝑖 ∈ ∅ ∣ ( ∅ “ { 𝑖 } ) ≠ { 𝑍 } } = ∅ )
9 3 6 8 3eqtrd ( 𝑍𝑊 → ( ∅ supp 𝑍 ) = ∅ )