Metamath Proof Explorer

Theorem elsuppfng

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

		Ref	Expression
	Assertion	elsuppfng	$⊢ (F Fn X \land F \in V \land Z \in W) \to (S \in {supp}_{Z} (F) \leftrightarrow (S \in X \land F (S) \neq Z))$

Proof

Step	Hyp	Ref	Expression
1		suppvalfng	$⊢ (F Fn X \land F \in V \land Z \in W) \to F supp Z = \{i \in X \| F (i) \neq Z\}$
2	1	eleq2d	$⊢ (F Fn X \land F \in V \land Z \in W) \to (S \in {supp}_{Z} (F) \leftrightarrow S \in \{i \in X \| F (i) \neq Z\})$
3		fveq2	$⊢ i = S \to F (i) = F (S)$
4	3	neeq1d	$⊢ i = S \to (F (i) \neq Z \leftrightarrow F (S) \neq Z)$
5	4	elrab	$⊢ S \in \{i \in X \| F (i) \neq Z\} \leftrightarrow (S \in X \land F (S) \neq Z)$
6	2 5	bitrdi	$⊢ (F Fn X \land F \in V \land Z \in W) \to (S \in {supp}_{Z} (F) \leftrightarrow (S \in X \land F (S) \neq Z))$