This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. V /\ Z e. W ) -> ( F supp Z ) = { i e. X | ( F ` i ) =/= Z } )

Proof

Step Hyp Ref Expression
1 fnfun 
 |-  ( F Fn X -> Fun F )
2 suppval1 
 |-  ( ( Fun F /\ F e. V /\ Z e. W ) -> ( F supp Z ) = { i e. dom F | ( F ` i ) =/= Z } )
3 1 2 syl3an1 
 |-  ( ( F Fn X /\ F e. V /\ Z e. W ) -> ( F supp Z ) = { i e. dom F | ( F ` i ) =/= Z } )
4 fndm 
 |-  ( F Fn X -> dom F = X )
5 4 3ad2ant1 
 |-  ( ( F Fn X /\ F e. V /\ Z e. W ) -> dom F = X )
6 5 rabeqdv 
 |-  ( ( F Fn X /\ F e. V /\ Z e. W ) -> { i e. dom F | ( F ` i ) =/= Z } = { i e. X | ( F ` i ) =/= Z } )
7 3 6 eqtrd 
 |-  ( ( F Fn X /\ F e. V /\ Z e. W ) -> ( F supp Z ) = { i e. X | ( F ` i ) =/= Z } )