Metamath Proof Explorer


Theorem elsuppfnd

Description: Deduce membership in the support of a function. (Contributed by Thierry Arnoux, 5-Oct-2025)

Ref Expression
Hypotheses elsuppfnd.1 φ F Fn A
elsuppfnd.2 φ A V
elsuppfnd.3 φ Z W
elsuppfnd.4 φ X A
elsuppfnd.5 φ F X Z
Assertion elsuppfnd φ X supp Z F

Proof

Step Hyp Ref Expression
1 elsuppfnd.1 φ F Fn A
2 elsuppfnd.2 φ A V
3 elsuppfnd.3 φ Z W
4 elsuppfnd.4 φ X A
5 elsuppfnd.5 φ F X Z
6 elsuppfn F Fn A A V Z W X supp Z F X A F X Z
7 6 biimpar F Fn A A V Z W X A F X Z X supp Z F
8 1 2 3 4 5 7 syl32anc φ X supp Z F