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 V F : I 0 F supp 0 = F -1

Proof

Step Hyp Ref Expression
1 c0ex 0 V
2 frnsuppeqg F V 0 V F : I 0 F supp 0 = F -1 0 0
3 1 2 mpan2 F V F : I 0 F supp 0 = F -1 0 0
4 3 imp F V F : I 0 F supp 0 = F -1 0 0
5 dfn2 = 0 0
6 5 imaeq2i F -1 = F -1 0 0
7 4 6 eqtr4di F V F : I 0 F supp 0 = F -1