Metamath Proof Explorer


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