Metamath Proof Explorer

Theorem res0

Description: A restriction to the empty set is empty. (Contributed by NM, 12-Nov-1994)

Ref Expression
Assertion res0 
|- ( A |` (/) ) = (/)

Proof

Step Hyp Ref Expression
1 df-res 
 |-  ( A |` (/) ) = ( A i^i ( (/) X. _V ) )
2 0xp 
 |-  ( (/) X. _V ) = (/)
3 2 ineq2i 
 |-  ( A i^i ( (/) X. _V ) ) = ( A i^i (/) )
4 in0 
 |-  ( A i^i (/) ) = (/)
5 1 3 4 3eqtri 
 |-  ( A |` (/) ) = (/)