Theorem nfimad

Description: Deduction version of bound-variable hypothesis builder nfima . (Contributed by FL, 15-Dec-2006) (Revised by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Hypotheses	nfimad.2	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
	nfimad.3	$$⊢\phi \to \underset{\_}{Ⅎ}xB$$
Assertion	nfimad	$$⊢\phi \to \underset{\_}{Ⅎ}xA\left[B\right]$$

Proof

Step	Hyp	Ref	Expression
1		nfimad.2	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
2		nfimad.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	nfima	$$⊢\underset{\_}{Ⅎ}x\left\{z|\forall xz\in A\right\}\left[\left\{z|\forall xz\in B\right\}\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	imaeq1d	$$⊢\underset{\_}{Ⅎ}xA\to \left\{z|\forall xz\in A\right\}\left[\left\{z|\forall xz\in B\right\}\right]=A\left[\left\{z|\forall xz\in B\right\}\right]$$
11		abidnf	$$⊢\underset{\_}{Ⅎ}xB\to \left\{z|\forall xz\in B\right\}=B$$
12	11	imaeq2d	$$⊢\underset{\_}{Ⅎ}xB\to A\left[\left\{z|\forall xz\in B\right\}\right]=A\left[B\right]$$
13	10 12	sylan9eq	$$⊢\left(\underset{\_}{Ⅎ}xA\wedge \underset{\_}{Ⅎ}xB\right)\to \left\{z|\forall xz\in A\right\}\left[\left\{z|\forall xz\in B\right\}\right]=A\left[B\right]$$
14	8 13	nfceqdf	$$⊢\left(\underset{\_}{Ⅎ}xA\wedge \underset{\_}{Ⅎ}xB\right)\to \left(\underset{\_}{Ⅎ}x\left\{z|\forall xz\in A\right\}\left[\left\{z|\forall xz\in B\right\}\right]\leftrightarrow \underset{\_}{Ⅎ}xA\left[B\right]\right)$$
15	1 2 14	syl2anc	$$⊢\phi \to \left(\underset{\_}{Ⅎ}x\left\{z|\forall xz\in A\right\}\left[\left\{z|\forall xz\in B\right\}\right]\leftrightarrow \underset{\_}{Ⅎ}xA\left[B\right]\right)$$
16	5 15	mpbii	$$⊢\phi \to \underset{\_}{Ⅎ}xA\left[B\right]$$