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	|- ( ph -> F/_ x F )
	nffvd.3	|- ( ph -> F/_ x A )
Assertion	nffvd	|- ( ph -> F/_ x ( F ` A ) )

Proof

Step	Hyp	Ref	Expression
1		nffvd.2	|- ( ph -> F/_ x F )
2		nffvd.3	|- ( ph -> F/_ x A )
3		nfaba1	|- F/_ x { z | A. x z e. F }
4		nfaba1	|- F/_ x { z | A. x z e. A }
5	3 4	nffv	|- F/_ x ( { z | A. x z e. F } ` { z | A. x z e. A } )
6		nfnfc1	|- F/ x F/_ x F
7		nfnfc1	|- F/ x F/_ x A
8	6 7	nfan	|- F/ x ( F/_ x F /\ F/_ x A )
9		abidnf	|- ( F/_ x F -> { z | A. x z e. F } = F )
10	9	adantr	|- ( ( F/_ x F /\ F/_ x A ) -> { z | A. x z e. F } = F )
11		abidnf	|- ( F/_ x A -> { z | A. x z e. A } = A )
12	11	adantl	|- ( ( F/_ x F /\ F/_ x A ) -> { z | A. x z e. A } = A )
13	10 12	fveq12d	|- ( ( F/_ x F /\ F/_ x A ) -> ( { z | A. x z e. F } ` { z | A. x z e. A } ) = ( F ` A ) )
14	8 13	nfceqdf	|- ( ( F/_ x F /\ F/_ x A ) -> ( F/_ x ( { z | A. x z e. F } ` { z | A. x z e. A } ) <-> F/_ x ( F ` A ) ) )
15	1 2 14	syl2anc	|- ( ph -> ( F/_ x ( { z | A. x z e. F } ` { z | A. x z e. A } ) <-> F/_ x ( F ` A ) ) )
16	5 15	mpbii	|- ( ph -> F/_ x ( F ` A ) )