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

Metamath Proof Explorer

Theorem inres

Description: Move intersection into class restriction. (Contributed by NM, 18-Dec-2008)

		Ref	Expression
	Assertion	inres	$⊢ A \cap ({B ↾}_{C}) = {(A \cap B) ↾}_{C}$

Step	Hyp	Ref	Expression
1		inass	$⊢ (A \cap B) \cap (C \times V) = A \cap (B \cap (C \times V))$
2		df-res	$⊢ {(A \cap B) ↾}_{C} = (A \cap B) \cap (C \times V)$
3		df-res	$⊢ {B ↾}_{C} = B \cap (C \times V)$
4	3	ineq2i	$⊢ A \cap ({B ↾}_{C}) = A \cap (B \cap (C \times V))$
5	1 2 4	3eqtr4ri	$⊢ A \cap ({B ↾}_{C}) = {(A \cap B) ↾}_{C}$