Metamath Proof Explorer


Theorem suppvalfng

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

Ref Expression
Assertion suppvalfng F Fn X F V Z W F supp Z = i X | F i Z

Proof

Step Hyp Ref Expression
1 fnfun F Fn X Fun F
2 suppval1 Fun F F V Z W F supp Z = i dom F | F i Z
3 1 2 syl3an1 F Fn X F V Z W F supp Z = i dom F | F i Z
4 fndm F Fn X dom F = X
5 4 3ad2ant1 F Fn X F V Z W dom F = X
6 5 rabeqdv F Fn X F V Z W i dom F | F i Z = i X | F i Z
7 3 6 eqtrd F Fn X F V Z W F supp Z = i X | F i Z