# Metamath Proof Explorer

## Theorem 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 ${⊢}\mathrm{ran}{B}\subseteq {C}\to \left({{A}↾}_{{C}}\right)\circ {B}={A}\circ {B}$

### Proof

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