Theorem suppssdm

Description: The support of a function is a subset of the function's domain. (Contributed by AV, 30-May-2019)

	Ref	Expression
Assertion	suppssdm	⊢ ( 𝐹 supp 𝑍 ) ⊆ dom 𝐹

Proof

Step	Hyp	Ref	Expression
1		suppval	⊢ ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) → ( 𝐹 supp 𝑍 ) = { 𝑖 ∈ dom 𝐹 ∣ ( 𝐹 “ { 𝑖 } ) ≠ { 𝑍 } } )
2		ssrab2	⊢ { 𝑖 ∈ dom 𝐹 ∣ ( 𝐹 “ { 𝑖 } ) ≠ { 𝑍 } } ⊆ dom 𝐹
3	1 2	eqsstrdi	⊢ ( ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) → ( 𝐹 supp 𝑍 ) ⊆ dom 𝐹 )
4		supp0prc	⊢ ( ¬ ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) → ( 𝐹 supp 𝑍 ) = ∅ )
5		0ss	⊢ ∅ ⊆ dom 𝐹
6	4 5	eqsstrdi	⊢ ( ¬ ( 𝐹 ∈ V ∧ 𝑍 ∈ V ) → ( 𝐹 supp 𝑍 ) ⊆ dom 𝐹 )
7	3 6	pm2.61i	⊢ ( 𝐹 supp 𝑍 ) ⊆ dom 𝐹