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

Metamath Proof Explorer

Theorem resmpt3

Description: Unconditional restriction of the mapping operation. (Contributed by Stefan O'Rear, 24-Jan-2015) (Proof shortened by Mario Carneiro, 22-Mar-2015)

		Ref	Expression
	Assertion	resmpt3	$⊢ {(x \in A ⟼ C) ↾}_{B} = (x \in (A \cap B) ⟼ C)$

Proof

Step	Hyp	Ref	Expression
1		resres	$⊢ {({(x \in A ⟼ C) ↾}_{A}) ↾}_{B} = {(x \in A ⟼ C) ↾}_{(A \cap B)}$
2		ssid	$⊢ A \subseteq A$
3		resmpt	$⊢ A \subseteq A \to {(x \in A ⟼ C) ↾}_{A} = (x \in A ⟼ C)$
4	2 3	ax-mp	$⊢ {(x \in A ⟼ C) ↾}_{A} = (x \in A ⟼ C)$
5	4	reseq1i	$⊢ {({(x \in A ⟼ C) ↾}_{A}) ↾}_{B} = {(x \in A ⟼ C) ↾}_{B}$
6		inss1	$⊢ A \cap B \subseteq A$
7		resmpt	$⊢ A \cap B \subseteq A \to {(x \in A ⟼ C) ↾}_{(A \cap B)} = (x \in (A \cap B) ⟼ C)$
8	6 7	ax-mp	$⊢ {(x \in A ⟼ C) ↾}_{(A \cap B)} = (x \in (A \cap B) ⟼ C)$
9	1 5 8	3eqtr3i	$⊢ {(x \in A ⟼ C) ↾}_{B} = (x \in (A \cap B) ⟼ C)$