Metamath Proof Explorer


Theorem elsuppfn

Description: An element of the support of a function with a given domain. (Contributed by AV, 27-May-2019)

Ref Expression
Assertion elsuppfn F Fn X X V Z W S supp Z F S X F S Z

Proof

Step Hyp Ref Expression
1 suppvalfn F Fn X X V Z W F supp Z = i X | F i Z
2 1 eleq2d F Fn X X V Z W S supp Z F S i X | F i Z
3 fveq2 i = S F i = F S
4 3 neeq1d i = S F i Z F S Z
5 4 elrab S i X | F i Z S X F S Z
6 2 5 bitrdi F Fn X X V Z W S supp Z F S X F S Z