Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Thierry Arnoux
Relations and Functions
Relations - misc additions
0res
Next ⟩
funresdm1
Metamath Proof Explorer
Ascii
Unicode
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
=
∅