# Metamath Proof Explorer

## Theorem nfopab

Description: Bound-variable hypothesis builder for class abstraction. (Contributed by NM, 1-Sep-1999) Remove disjoint variable conditions. (Revised by Andrew Salmon, 11-Jul-2011)

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

### Proof

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