Metamath Proof Explorer


Theorem resdifcom

Description: Commutative law for restriction and difference. (Contributed by AV, 7-Jun-2021)

Ref Expression
Assertion resdifcom ABC=ACB

Proof

Step Hyp Ref Expression
1 indif1 ACB×V=AB×VC
2 df-res ACB=ACB×V
3 df-res AB=AB×V
4 3 difeq1i ABC=AB×VC
5 1 2 4 3eqtr4ri ABC=ACB