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	$⊢ F supp Z \subseteq dom F$

Step	Hyp	Ref	Expression
1		suppval	$⊢ (F \in V \land Z \in V) \to F supp Z = \{i \in dom F \| F [\{i\}] \neq \{Z\}\}$
2		ssrab2	$⊢ \{i \in dom F \| F [\{i\}] \neq \{Z\}\} \subseteq dom F$
3	1 2	eqsstrdi	$⊢ (F \in V \land Z \in V) \to F supp Z \subseteq dom F$
4		supp0prc	$⊢ \neg (F \in V \land Z \in V) \to F supp Z = \emptyset$
5		0ss	$⊢ \emptyset \subseteq dom F$
6	4 5	eqsstrdi	$⊢ \neg (F \in V \land Z \in V) \to F supp Z \subseteq dom F$
7	3 6	pm2.61i	$⊢ F supp Z \subseteq dom F$

Metamath Proof Explorer