Metamath Proof Explorer


Theorem 0res

Description: Restriction of the empty function. (Contributed by Thierry Arnoux, 20-Nov-2023)

Ref Expression
Assertion 0res A =

Proof

Step Hyp Ref Expression
1 df-res A = A × V
2 0in A × V =
3 1 2 eqtri A =