Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Power Sets
Relations
resabs2
Next ⟩
residm
Metamath Proof Explorer
Ascii
Unicode
Theorem
resabs2
Description:
Absorption law for restriction.
(Contributed by
NM
, 27-Mar-1998)
Ref
Expression
Assertion
resabs2
⊢
B
⊆
C
→
A
↾
B
↾
C
=
A
↾
B
Proof
Step
Hyp
Ref
Expression
1
rescom
⊢
A
↾
B
↾
C
=
A
↾
C
↾
B
2
resabs1
⊢
B
⊆
C
→
A
↾
C
↾
B
=
A
↾
B
3
1
2
eqtrid
⊢
B
⊆
C
→
A
↾
B
↾
C
=
A
↾
B