Metamath Proof Explorer


Theorem relfsupp

Description: The property of a function to be finitely supported is a relation. (Contributed by AV, 7-Jun-2019)

Ref Expression
Assertion relfsupp Rel finSupp

Proof

Step Hyp Ref Expression
1 df-fsupp finSupp = r z | Fun r r supp z Fin
2 1 relopabiv Rel finSupp