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	|- ( ph -> F/_ x A )
	nfimad.3	|- ( ph -> F/_ x B )
Assertion	nfimad	|- ( ph -> F/_ x ( A " B ) )

Proof

Step	Hyp	Ref	Expression
1		nfimad.2	|- ( ph -> F/_ x A )
2		nfimad.3	|- ( ph -> F/_ x B )
3		nfaba1	|- F/_ x { z | A. x z e. A }
4		nfaba1	|- F/_ x { z | A. x z e. B }
5	3 4	nfima	|- F/_ x ( { z | A. x z e. A } " { z | A. x z e. B } )
6		nfnfc1	|- F/ x F/_ x A
7		nfnfc1	|- F/ x F/_ x B
8	6 7	nfan	|- F/ x ( F/_ x A /\ F/_ x B )
9		abidnf	|- ( F/_ x A -> { z | A. x z e. A } = A )
10	9	imaeq1d	|- ( F/_ x A -> ( { z | A. x z e. A } " { z | A. x z e. B } ) = ( A " { z | A. x z e. B } ) )
11		abidnf	|- ( F/_ x B -> { z | A. x z e. B } = B )
12	11	imaeq2d	|- ( F/_ x B -> ( A " { z | A. x z e. B } ) = ( A " B ) )
13	10 12	sylan9eq	|- ( ( F/_ x A /\ F/_ x B ) -> ( { z | A. x z e. A } " { z | A. x z e. B } ) = ( A " B ) )
14	8 13	nfceqdf	|- ( ( F/_ x A /\ F/_ x B ) -> ( F/_ x ( { z | A. x z e. A } " { z | A. x z e. B } ) <-> F/_ x ( A " B ) ) )
15	1 2 14	syl2anc	|- ( ph -> ( F/_ x ( { z | A. x z e. A } " { z | A. x z e. B } ) <-> F/_ x ( A " B ) ) )
16	5 15	mpbii	|- ( ph -> F/_ x ( A " B ) )