# Metamath Proof Explorer

## Theorem nfop

Description: Bound-variable hypothesis builder for ordered pairs. (Contributed by NM, 14-Nov-1995)

Ref Expression
Hypotheses nfop.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
nfop.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
Assertion nfop ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}⟨{A},{B}⟩$

### Proof

Step Hyp Ref Expression
1 nfop.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
2 nfop.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
3 dfopif ${⊢}⟨{A},{B}⟩=if\left(\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right),\left\{\left\{{A}\right\},\left\{{A},{B}\right\}\right\},\varnothing \right)$
4 1 nfel1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{A}\in \mathrm{V}$
5 2 nfel1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{B}\in \mathrm{V}$
6 4 5 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right)$
7 1 nfsn ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{{A}\right\}$
8 1 2 nfpr ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{{A},{B}\right\}$
9 7 8 nfpr ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{\left\{{A}\right\},\left\{{A},{B}\right\}\right\}$
10 nfcv ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\varnothing$
11 6 9 10 nfif ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}if\left(\left({A}\in \mathrm{V}\wedge {B}\in \mathrm{V}\right),\left\{\left\{{A}\right\},\left\{{A},{B}\right\}\right\},\varnothing \right)$
12 3 11 nfcxfr ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}⟨{A},{B}⟩$