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