fdifsupp

Description: Express the support of a function F outside of B in two different ways. (Contributed by Thierry Arnoux, 5-Oct-2025)

	Ref	Expression
Hypotheses	fdifsupp.1	$⊢ φ \to A \in V$
	fdifsupp.2	$⊢ φ \to Z \in W$
	fdifsupp.3	$⊢ φ \to F Fn A$
Assertion	fdifsupp	$⊢ φ \to ({F ↾}_{(A ∖ B)}) supp Z = {supp}_{Z} (F) ∖ B$

Proof

Step	Hyp	Ref	Expression
1		fdifsupp.1	$⊢ φ \to A \in V$
2		fdifsupp.2	$⊢ φ \to Z \in W$
3		fdifsupp.3	$⊢ φ \to F Fn A$
4		difssd	$⊢ φ \to A ∖ B \subseteq A$
5	3 4	fnssresd	$⊢ φ \to ({F ↾}_{(A ∖ B)}) Fn (A ∖ B)$
6	1	difexd	$⊢ φ \to A ∖ B \in V$
7		elsuppfn	$⊢ (({F ↾}_{(A ∖ B)}) Fn (A ∖ B) \land A ∖ B \in V \land Z \in W) \to (x \in {supp}_{Z} (({F ↾}_{(A ∖ B)})) \leftrightarrow (x \in (A ∖ B) \land ({F ↾}_{(A ∖ B)}) (x) \neq Z))$
8	5 6 2 7	syl3anc	$⊢ φ \to (x \in {supp}_{Z} (({F ↾}_{(A ∖ B)})) \leftrightarrow (x \in (A ∖ B) \land ({F ↾}_{(A ∖ B)}) (x) \neq Z))$
9		eldif	$⊢ x \in (A ∖ B) \leftrightarrow (x \in A \land \neg x \in B)$
10	9	anbi1i	$⊢ (x \in (A ∖ B) \land F (x) \neq Z) \leftrightarrow ((x \in A \land \neg x \in B) \land F (x) \neq Z)$
11	10	a1i	$⊢ φ \to ((x \in (A ∖ B) \land F (x) \neq Z) \leftrightarrow ((x \in A \land \neg x \in B) \land F (x) \neq Z))$
12		simpr	$⊢ (φ \land x \in (A ∖ B)) \to x \in (A ∖ B)$
13	12	fvresd	$⊢ (φ \land x \in (A ∖ B)) \to ({F ↾}_{(A ∖ B)}) (x) = F (x)$
14	13	neeq1d	$⊢ (φ \land x \in (A ∖ B)) \to (({F ↾}_{(A ∖ B)}) (x) \neq Z \leftrightarrow F (x) \neq Z)$
15	14	pm5.32da	$⊢ φ \to ((x \in (A ∖ B) \land ({F ↾}_{(A ∖ B)}) (x) \neq Z) \leftrightarrow (x \in (A ∖ B) \land F (x) \neq Z))$
16		an32	$⊢ ((x \in A \land F (x) \neq Z) \land \neg x \in B) \leftrightarrow ((x \in A \land \neg x \in B) \land F (x) \neq Z)$
17	16	a1i	$⊢ φ \to (((x \in A \land F (x) \neq Z) \land \neg x \in B) \leftrightarrow ((x \in A \land \neg x \in B) \land F (x) \neq Z))$
18	11 15 17	3bitr4d	$⊢ φ \to ((x \in (A ∖ B) \land ({F ↾}_{(A ∖ B)}) (x) \neq Z) \leftrightarrow ((x \in A \land F (x) \neq Z) \land \neg x \in B))$
19		eldif	$⊢ x \in ({supp}_{Z} (F) ∖ B) \leftrightarrow (x \in {supp}_{Z} (F) \land \neg x \in B)$
20	1	elexd	$⊢ φ \to A \in V$
21		elsuppfn	$⊢ (F Fn A \land A \in V \land Z \in W) \to (x \in {supp}_{Z} (F) \leftrightarrow (x \in A \land F (x) \neq Z))$
22	3 20 2 21	syl3anc	$⊢ φ \to (x \in {supp}_{Z} (F) \leftrightarrow (x \in A \land F (x) \neq Z))$
23	22	anbi1d	$⊢ φ \to ((x \in {supp}_{Z} (F) \land \neg x \in B) \leftrightarrow ((x \in A \land F (x) \neq Z) \land \neg x \in B))$
24	19 23	bitr2id	$⊢ φ \to (((x \in A \land F (x) \neq Z) \land \neg x \in B) \leftrightarrow x \in ({supp}_{Z} (F) ∖ B))$
25	8 18 24	3bitrd	$⊢ φ \to (x \in {supp}_{Z} (({F ↾}_{(A ∖ B)})) \leftrightarrow x \in ({supp}_{Z} (F) ∖ B))$
26	25	eqrdv	$⊢ φ \to ({F ↾}_{(A ∖ B)}) supp Z = {supp}_{Z} (F) ∖ B$

Metamath Proof Explorer

Theorem fdifsupp

Proof