# Metamath Proof Explorer

## Theorem nfco

Description: Bound-variable hypothesis builder for function value. (Contributed by NM, 1-Sep-1999)

Ref Expression
Hypotheses nfco.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
nfco.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
Assertion nfco ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({A}\circ {B}\right)$

### Proof

Step Hyp Ref Expression
1 nfco.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
2 nfco.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
3 df-co ${⊢}{A}\circ {B}=\left\{⟨{y},{z}⟩|\exists {w}\phantom{\rule{.4em}{0ex}}\left({y}{B}{w}\wedge {w}{A}{z}\right)\right\}$
4 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{y}$
5 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{w}$
6 4 2 5 nfbr ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}{B}{w}$
7 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{z}$
8 5 1 7 nfbr ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{w}{A}{z}$
9 6 8 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({y}{B}{w}\wedge {w}{A}{z}\right)$
10 9 nfex ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\exists {w}\phantom{\rule{.4em}{0ex}}\left({y}{B}{w}\wedge {w}{A}{z}\right)$
11 10 nfopab ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{⟨{y},{z}⟩|\exists {w}\phantom{\rule{.4em}{0ex}}\left({y}{B}{w}\wedge {w}{A}{z}\right)\right\}$
12 3 11 nfcxfr ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({A}\circ {B}\right)$