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	⊢ ( ( 𝐵 ↾ ran 𝐴 ) ∘ 𝐴 ) = ( 𝐵 ∘ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2		vex	⊢ 𝑦 ∈ V
3	1 2	brelrn	⊢ ( 𝑥 𝐴 𝑦 → 𝑦 ∈ ran 𝐴 )
4		vex	⊢ 𝑧 ∈ V
5	4	brresi	⊢ ( 𝑦 ( 𝐵 ↾ ran 𝐴 ) 𝑧 ↔ ( 𝑦 ∈ ran 𝐴 ∧ 𝑦 𝐵 𝑧 ) )
6	5	baib	⊢ ( 𝑦 ∈ ran 𝐴 → ( 𝑦 ( 𝐵 ↾ ran 𝐴 ) 𝑧 ↔ 𝑦 𝐵 𝑧 ) )
7	3 6	syl	⊢ ( 𝑥 𝐴 𝑦 → ( 𝑦 ( 𝐵 ↾ ran 𝐴 ) 𝑧 ↔ 𝑦 𝐵 𝑧 ) )
8	7	pm5.32i	⊢ ( ( 𝑥 𝐴 𝑦 ∧ 𝑦 ( 𝐵 ↾ ran 𝐴 ) 𝑧 ) ↔ ( 𝑥 𝐴 𝑦 ∧ 𝑦 𝐵 𝑧 ) )
9	8	exbii	⊢ ( ∃ 𝑦 ( 𝑥 𝐴 𝑦 ∧ 𝑦 ( 𝐵 ↾ ran 𝐴 ) 𝑧 ) ↔ ∃ 𝑦 ( 𝑥 𝐴 𝑦 ∧ 𝑦 𝐵 𝑧 ) )
10	9	opabbii	⊢ { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( 𝑥 𝐴 𝑦 ∧ 𝑦 ( 𝐵 ↾ ran 𝐴 ) 𝑧 ) } = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( 𝑥 𝐴 𝑦 ∧ 𝑦 𝐵 𝑧 ) }
11		df-co	⊢ ( ( 𝐵 ↾ ran 𝐴 ) ∘ 𝐴 ) = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( 𝑥 𝐴 𝑦 ∧ 𝑦 ( 𝐵 ↾ ran 𝐴 ) 𝑧 ) }
12		df-co	⊢ ( 𝐵 ∘ 𝐴 ) = { ⟨ 𝑥 , 𝑧 ⟩ ∣ ∃ 𝑦 ( 𝑥 𝐴 𝑦 ∧ 𝑦 𝐵 𝑧 ) }
13	10 11 12	3eqtr4i	⊢ ( ( 𝐵 ↾ ran 𝐴 ) ∘ 𝐴 ) = ( 𝐵 ∘ 𝐴 )