This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem resdifdir

Description: Distributive law for restriction over difference. (Contributed by BTernaryTau, 15-Aug-2024)

		Ref	Expression
	Assertion	resdifdir	$⊢ {(A ∖ B) ↾}_{C} = ({A ↾}_{C}) ∖ ({B ↾}_{C})$

Step	Hyp	Ref	Expression
1		indifdir	$⊢ (A ∖ B) \cap (C \times V) = (A \cap (C \times V)) ∖ (B \cap (C \times V))$
2		df-res	$⊢ {(A ∖ B) ↾}_{C} = (A ∖ B) \cap (C \times V)$
3		df-res	$⊢ {A ↾}_{C} = A \cap (C \times V)$
4		df-res	$⊢ {B ↾}_{C} = B \cap (C \times V)$
5	3 4	difeq12i	$⊢ ({A ↾}_{C}) ∖ ({B ↾}_{C}) = (A \cap (C \times V)) ∖ (B \cap (C \times V))$
6	1 2 5	3eqtr4i	$⊢ {(A ∖ B) ↾}_{C} = ({A ↾}_{C}) ∖ ({B ↾}_{C})$