Metamath Proof Explorer

Theorem frnnn0suppg

Description: Version of frnnn0supp avoiding ax-rep by assuming F is a set rather than its domain I . (Contributed by SN, 5-Aug-2024)

Ref Expression
Assertion frnnn0suppg 
|- ( ( F e. V /\ F : I --> NN0 ) -> ( F supp 0 ) = ( `' F " NN ) )

Proof

Step Hyp Ref Expression
1 c0ex 
 |-  0 e. _V
2 frnsuppeqg 
 |-  ( ( F e. V /\ 0 e. _V ) -> ( F : I --> NN0 -> ( F supp 0 ) = ( `' F " ( NN0 \ { 0 } ) ) ) )
3 1 2 mpan2 
 |-  ( F e. V -> ( F : I --> NN0 -> ( F supp 0 ) = ( `' F " ( NN0 \ { 0 } ) ) ) )
4 3 imp 
 |-  ( ( F e. V /\ F : I --> NN0 ) -> ( F supp 0 ) = ( `' F " ( NN0 \ { 0 } ) ) )
5 dfn2 
 |-  NN = ( NN0 \ { 0 } )
6 5 imaeq2i 
 |-  ( `' F " NN ) = ( `' F " ( NN0 \ { 0 } ) )
7 4 6 eqtr4di 
 |-  ( ( F e. V /\ F : I --> NN0 ) -> ( F supp 0 ) = ( `' F " NN ) )