Theorem resdifcom

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

	Ref	Expression
Assertion	resdifcom	⊢ ( ( 𝐴 ↾ 𝐵 ) ∖ 𝐶 ) = ( ( 𝐴 ∖ 𝐶 ) ↾ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		indif1	⊢ ( ( 𝐴 ∖ 𝐶 ) ∩ ( 𝐵 × V ) ) = ( ( 𝐴 ∩ ( 𝐵 × V ) ) ∖ 𝐶 )
2		df-res	⊢ ( ( 𝐴 ∖ 𝐶 ) ↾ 𝐵 ) = ( ( 𝐴 ∖ 𝐶 ) ∩ ( 𝐵 × V ) )
3		df-res	⊢ ( 𝐴 ↾ 𝐵 ) = ( 𝐴 ∩ ( 𝐵 × V ) )
4	3	difeq1i	⊢ ( ( 𝐴 ↾ 𝐵 ) ∖ 𝐶 ) = ( ( 𝐴 ∩ ( 𝐵 × V ) ) ∖ 𝐶 )
5	1 2 4	3eqtr4ri	⊢ ( ( 𝐴 ↾ 𝐵 ) ∖ 𝐶 ) = ( ( 𝐴 ∖ 𝐶 ) ↾ 𝐵 )