resdifdi

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

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

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

Metamath Proof Explorer