Metamath Proof Explorer


Theorem 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 φ A V
fdifsupp.2 φ Z W
fdifsupp.3 φ F Fn A
Assertion fdifsupp φ F A B supp Z = supp Z F B

Proof

Step Hyp Ref Expression
1 fdifsupp.1 φ A V
2 fdifsupp.2 φ Z W
3 fdifsupp.3 φ F Fn A
4 difssd φ A B A
5 3 4 fnssresd φ F A B Fn A B
6 1 difexd φ A B V
7 elsuppfn F A B Fn A B A B V Z W x supp Z F A B x A B F A B x Z
8 5 6 2 7 syl3anc φ x supp Z F A B x A B F A B x Z
9 eldif x A B x A ¬ x B
10 9 anbi1i x A B F x Z x A ¬ x B F x Z
11 10 a1i φ x A B F x Z x A ¬ x B F x Z
12 simpr φ x A B x A B
13 12 fvresd φ x A B F A B x = F x
14 13 neeq1d φ x A B F A B x Z F x Z
15 14 pm5.32da φ x A B F A B x Z x A B F x Z
16 an32 x A F x Z ¬ x B x A ¬ x B F x Z
17 16 a1i φ x A F x Z ¬ x B x A ¬ x B F x Z
18 11 15 17 3bitr4d φ x A B F A B x Z x A F x Z ¬ x B
19 eldif x supp Z F B x supp Z F ¬ x B
20 1 elexd φ A V
21 elsuppfn F Fn A A V Z W x supp Z F x A F x Z
22 3 20 2 21 syl3anc φ x supp Z F x A F x Z
23 22 anbi1d φ x supp Z F ¬ x B x A F x Z ¬ x B
24 19 23 bitr2id φ x A F x Z ¬ x B x supp Z F B
25 8 18 24 3bitrd φ x supp Z F A B x supp Z F B
26 25 eqrdv φ F A B supp Z = supp Z F B