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	⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
	nfifd.3	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
	nfifd.4	⊢ ( 𝜑 → Ⅎ 𝑥 𝐵 )
Assertion	nfifd	⊢ ( 𝜑 → Ⅎ 𝑥 if ( 𝜓 , 𝐴 , 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		nfifd.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝜓 )
2		nfifd.3	⊢ ( 𝜑 → Ⅎ 𝑥 𝐴 )
3		nfifd.4	⊢ ( 𝜑 → Ⅎ 𝑥 𝐵 )
4		dfif2	⊢ if ( 𝜓 , 𝐴 , 𝐵 ) = { 𝑦 ∣ ( ( 𝑦 ∈ 𝐵 → 𝜓 ) → ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) }
5		nfv	⊢ Ⅎ 𝑦 𝜑
6	3	nfcrd	⊢ ( 𝜑 → Ⅎ 𝑥 𝑦 ∈ 𝐵 )
7	6 1	nfimd	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝑦 ∈ 𝐵 → 𝜓 ) )
8	2	nfcrd	⊢ ( 𝜑 → Ⅎ 𝑥 𝑦 ∈ 𝐴 )
9	8 1	nfand	⊢ ( 𝜑 → Ⅎ 𝑥 ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) )
10	7 9	nfimd	⊢ ( 𝜑 → Ⅎ 𝑥 ( ( 𝑦 ∈ 𝐵 → 𝜓 ) → ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) )
11	5 10	nfabdw	⊢ ( 𝜑 → Ⅎ 𝑥 { 𝑦 ∣ ( ( 𝑦 ∈ 𝐵 → 𝜓 ) → ( 𝑦 ∈ 𝐴 ∧ 𝜓 ) ) } )
12	4 11	nfcxfrd	⊢ ( 𝜑 → Ⅎ 𝑥 if ( 𝜓 , 𝐴 , 𝐵 ) )