cores

Description: Restricted first member of a class composition. (Contributed by NM, 12-Oct-2004) (Proof shortened by Andrew Salmon, 27-Aug-2011)

		Ref	Expression
	Assertion	cores	$⊢ ran B \subseteq C \to ({A ↾}_{C}) \circ B = A \circ B$

Step	Hyp	Ref	Expression
1		vex	$⊢ z \in V$
2		vex	$⊢ y \in V$
3	1 2	brelrn	$⊢ z B y \to y \in ran B$
4		ssel	$⊢ ran B \subseteq C \to (y \in ran B \to y \in C)$
5		vex	$⊢ x \in V$
6	5	brresi	$⊢ y ({A ↾}_{C}) x \leftrightarrow (y \in C \land y A x)$
7	6	baib	$⊢ y \in C \to (y ({A ↾}_{C}) x \leftrightarrow y A x)$
8	3 4 7	syl56	$⊢ ran B \subseteq C \to (z B y \to (y ({A ↾}_{C}) x \leftrightarrow y A x))$
9	8	pm5.32d	$⊢ ran B \subseteq C \to ((z B y \land y ({A ↾}_{C}) x) \leftrightarrow (z B y \land y A x))$
10	9	exbidv	$⊢ ran B \subseteq C \to (\exists y (z B y \land y ({A ↾}_{C}) x) \leftrightarrow \exists y (z B y \land y A x))$
11	10	opabbidv	$⊢ ran B \subseteq C \to \{⟨z, x⟩ \| \exists y (z B y \land y ({A ↾}_{C}) x)\} = \{⟨z, x⟩ \| \exists y (z B y \land y A x)\}$
12		df-co	$⊢ ({A ↾}_{C}) \circ B = \{⟨z, x⟩ \| \exists y (z B y \land y ({A ↾}_{C}) x)\}$
13		df-co	$⊢ A \circ B = \{⟨z, x⟩ \| \exists y (z B y \land y A x)\}$
14	11 12 13	3eqtr4g	$⊢ ran B \subseteq C \to ({A ↾}_{C}) \circ B = A \circ B$

Metamath Proof Explorer