# Metamath Proof Explorer

## Theorem nfopd

Description: Deduction version of bound-variable hypothesis builder nfop . This shows how the deduction version of a not-free theorem such as nfop can be created from the corresponding not-free inference theorem. (Contributed by NM, 4-Feb-2008)

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

### Proof

Step Hyp Ref Expression
1 nfopd.2 ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
2 nfopd.3 ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
3 nfaba1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}{z}\in {A}\right\}$
4 nfaba1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}{z}\in {B}\right\}$
5 3 4 nfop ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}⟨\left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}{z}\in {A}\right\},\left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}{z}\in {B}\right\}⟩$
6 nfnfc1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
7 nfnfc1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
8 6 7 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left(\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\wedge \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}\right)$
9 abidnf ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\to \left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}{z}\in {A}\right\}={A}$
10 9 adantr ${⊢}\left(\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\wedge \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}\right)\to \left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}{z}\in {A}\right\}={A}$
11 abidnf ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}\to \left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}{z}\in {B}\right\}={B}$
12 11 adantl ${⊢}\left(\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\wedge \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}\right)\to \left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}{z}\in {B}\right\}={B}$
13 10 12 opeq12d ${⊢}\left(\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\wedge \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}\right)\to ⟨\left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}{z}\in {A}\right\},\left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}{z}\in {B}\right\}⟩=⟨{A},{B}⟩$
14 8 13 nfceqdf ${⊢}\left(\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}\wedge \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}\right)\to \left(\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}⟨\left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}{z}\in {A}\right\},\left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}{z}\in {B}\right\}⟩↔\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}⟨{A},{B}⟩\right)$
15 1 2 14 syl2anc ${⊢}{\phi }\to \left(\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}⟨\left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}{z}\in {A}\right\},\left\{{z}|\forall {x}\phantom{\rule{.4em}{0ex}}{z}\in {B}\right\}⟩↔\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}⟨{A},{B}⟩\right)$
16 5 15 mpbii ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}⟨{A},{B}⟩$