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

Metamath Proof Explorer

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