This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )