Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Glauco Siliprandi
Miscellanea
resabs2i
Next ⟩
ssdf2
Metamath Proof Explorer
Ascii
Unicode
Theorem
resabs2i
Description:
Absorption law for restriction.
(Contributed by
Glauco Siliprandi
, 2-Jan-2022)
Ref
Expression
Hypothesis
resabs2i.1
⊢
B
⊆
C
Assertion
resabs2i
⊢
A
↾
B
↾
C
=
A
↾
B
Proof
Step
Hyp
Ref
Expression
1
resabs2i.1
⊢
B
⊆
C
2
resabs2
⊢
B
⊆
C
→
A
↾
B
↾
C
=
A
↾
B
3
1
2
ax-mp
⊢
A
↾
B
↾
C
=
A
↾
B