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 𝑍 ) = ∅ )