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 ) = ( (/) i^i ( A X. _V ) )
2 0in 
 |-  ( (/) i^i ( A X. _V ) ) = (/)
3 1 2 eqtri 
 |-  ( (/) |` A ) = (/)