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

Metamath Proof Explorer

Theorem nfifd

Description: Deduction form of nfif . (Contributed by NM, 15-Feb-2013) (Revised by Mario Carneiro, 13-Oct-2016)

Ref Expression
Hypotheses nfifd.2 
|- ( ph -> F/ x ps )
nfifd.3 
|- ( ph -> F/_ x A )
nfifd.4 
|- ( ph -> F/_ x B )
Assertion nfifd 
|- ( ph -> F/_ x if ( ps , A , B ) )

Proof

Step Hyp Ref Expression
1 nfifd.2 
 |-  ( ph -> F/ x ps )
2 nfifd.3 
 |-  ( ph -> F/_ x A )
3 nfifd.4 
 |-  ( ph -> F/_ x B )
4 dfif2 
 |-  if ( ps , A , B ) = { y | ( ( y e. B -> ps ) -> ( y e. A /\ ps ) ) }
5 nfv 
 |-  F/ y ph
6 3 nfcrd 
 |-  ( ph -> F/ x y e. B )
7 6 1 nfimd 
 |-  ( ph -> F/ x ( y e. B -> ps ) )
8 2 nfcrd 
 |-  ( ph -> F/ x y e. A )
9 8 1 nfand 
 |-  ( ph -> F/ x ( y e. A /\ ps ) )
10 7 9 nfimd 
 |-  ( ph -> F/ x ( ( y e. B -> ps ) -> ( y e. A /\ ps ) ) )
11 5 10 nfabdw 
 |-  ( ph -> F/_ x { y | ( ( y e. B -> ps ) -> ( y e. A /\ ps ) ) } )
12 4 11 nfcxfrd 
 |-  ( ph -> F/_ x if ( ps , A , B ) )