Metamath Proof Explorer

Theorem coresrn

Description: When composing classes, restricting the second class to the range of the first has no effect. (Contributed by BJ, 22-Oct-2026) Note: can be moved before cores and shorten funresfunco , dprdf1 , kgencn2 , domss2 .

		Ref	Expression
	Assertion	coresrn	$⊢ ({B ↾}_{ran A}) \circ A = B \circ A$

Proof

Step	Hyp	Ref	Expression
1		vex	$⊢ x \in V$
2		vex	$⊢ y \in V$
3	1 2	brelrn	$⊢ x A y \to y \in ran A$
4		vex	$⊢ z \in V$
5	4	brresi	$⊢ y ({B ↾}_{ran A}) z \leftrightarrow (y \in ran A \land y B z)$
6	5	baib	$⊢ y \in ran A \to (y ({B ↾}_{ran A}) z \leftrightarrow y B z)$
7	3 6	syl	$⊢ x A y \to (y ({B ↾}_{ran A}) z \leftrightarrow y B z)$
8	7	pm5.32i	$⊢ (x A y \land y ({B ↾}_{ran A}) z) \leftrightarrow (x A y \land y B z)$
9	8	exbii	$⊢ \exists y (x A y \land y ({B ↾}_{ran A}) z) \leftrightarrow \exists y (x A y \land y B z)$
10	9	opabbii	$⊢ \{⟨x, z⟩ \| \exists y (x A y \land y ({B ↾}_{ran A}) z)\} = \{⟨x, z⟩ \| \exists y (x A y \land y B z)\}$
11		df-co	$⊢ ({B ↾}_{ran A}) \circ A = \{⟨x, z⟩ \| \exists y (x A y \land y ({B ↾}_{ran A}) z)\}$
12		df-co	$⊢ B \circ A = \{⟨x, z⟩ \| \exists y (x A y \land y B z)\}$
13	10 11 12	3eqtr4i	$⊢ ({B ↾}_{ran A}) \circ A = B \circ A$