suppvalfng

Description: The value of the operation constructing the support of a function with a given domain. This version of suppvalfn assumes F is a set rather than its domain X , avoiding ax-rep . (Contributed by SN, 5-Aug-2024)

		Ref	Expression
	Assertion	suppvalfng	$⊢ (F Fn X \land F \in V \land Z \in W) \to F supp Z = \{i \in X \| F (i) \neq Z\}$

Proof

Step	Hyp	Ref	Expression
1		fnfun	$⊢ F Fn X \to Fun F$
2		suppval1	$⊢ (Fun F \land F \in V \land Z \in W) \to F supp Z = \{i \in dom F \| F (i) \neq Z\}$
3	1 2	syl3an1	$⊢ (F Fn X \land F \in V \land Z \in W) \to F supp Z = \{i \in dom F \| F (i) \neq Z\}$
4		fndm	$⊢ F Fn X \to dom F = X$
5	4	3ad2ant1	$⊢ (F Fn X \land F \in V \land Z \in W) \to dom F = X$
6	5	rabeqdv	$⊢ (F Fn X \land F \in V \land Z \in W) \to \{i \in dom F \| F (i) \neq Z\} = \{i \in X \| F (i) \neq Z\}$
7	3 6	eqtrd	$⊢ (F Fn X \land F \in V \land Z \in W) \to F supp Z = \{i \in X \| F (i) \neq Z\}$

Metamath Proof Explorer

Theorem suppvalfng

Proof