Theorem nfopdALT

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, 19-Nov-2020) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nfopdALT.1	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
	nfopdALT.2	$$⊢\phi \to \underset{\_}{Ⅎ}xB$$
Assertion	nfopdALT	$$⊢\phi \to \underset{\_}{Ⅎ}x⟨A,B⟩$$

Proof

Step	Hyp	Ref	Expression
1		nfopdALT.1	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
2		nfopdALT.2	$$⊢\phi \to \underset{\_}{Ⅎ}xB$$
3		abidnf	$$⊢\underset{\_}{Ⅎ}xA\to \left\{z|\forall xz\in A\right\}=A$$
4	3	adantr	$$⊢\left(\underset{\_}{Ⅎ}xA\wedge \underset{\_}{Ⅎ}xB\right)\to \left\{z|\forall xz\in A\right\}=A$$
5		abidnf	$$⊢\underset{\_}{Ⅎ}xB\to \left\{z|\forall xz\in B\right\}=B$$
6	5	adantl	$$⊢\left(\underset{\_}{Ⅎ}xA\wedge \underset{\_}{Ⅎ}xB\right)\to \left\{z|\forall xz\in B\right\}=B$$
7	4 6	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⟩$$
8		nfaba1	$$⊢\underset{\_}{Ⅎ}x\left\{z|\forall xz\in A\right\}$$
9		nfaba1	$$⊢\underset{\_}{Ⅎ}x\left\{z|\forall xz\in B\right\}$$
10	8 9	nfop	$$⊢\underset{\_}{Ⅎ}x⟨\left\{z|\forall xz\in A\right\},\left\{z|\forall xz\in B\right\}⟩$$
11	1 2 7 10	nfded2	$$⊢\phi \to \underset{\_}{Ⅎ}x⟨A,B⟩$$