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{\_}{Ⅎ}xA$$
	nfopd.3	$$⊢\phi \to \underset{\_}{Ⅎ}xB$$
Assertion	nfopd	$$⊢\phi \to \underset{\_}{Ⅎ}x⟨A,B⟩$$

Proof

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