# Metamath Proof Explorer

## Theorem nfoprab2

Description: The abstraction variables in an operation class abstraction are not free. (Contributed by NM, 25-Apr-1995) (Revised by David Abernethy, 30-Jul-2012)

Ref Expression
Assertion nfoprab2 ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left\{⟨⟨{x},{y}⟩,{z}⟩|{\phi }\right\}$

### Proof

Step Hyp Ref Expression
1 df-oprab ${⊢}\left\{⟨⟨{x},{y}⟩,{z}⟩|{\phi }\right\}=\left\{{w}|\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨⟨{x},{y}⟩,{z}⟩\wedge {\phi }\right)\right\}$
2 nfe1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨⟨{x},{y}⟩,{z}⟩\wedge {\phi }\right)$
3 2 nfex ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨⟨{x},{y}⟩,{z}⟩\wedge {\phi }\right)$
4 3 nfab ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left\{{w}|\exists {x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({w}=⟨⟨{x},{y}⟩,{z}⟩\wedge {\phi }\right)\right\}$
5 1 4 nfcxfr ${⊢}\underset{_}{Ⅎ}{y}\phantom{\rule{.4em}{0ex}}\left\{⟨⟨{x},{y}⟩,{z}⟩|{\phi }\right\}$