Theorem nffvd

Description: Deduction version of bound-variable hypothesis builder nffv . (Contributed by NM, 10-Nov-2005) (Revised by Mario Carneiro, 15-Oct-2016)

	Ref	Expression
Hypotheses	nffvd.2	$$⊢\phi \to \underset{\_}{Ⅎ}xF$$
	nffvd.3	$$⊢\phi \to \underset{\_}{Ⅎ}xA$$
Assertion	nffvd	$$⊢\phi \to \underset{\_}{Ⅎ}xF\left(A\right)$$

Proof

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