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 φ x ψ
nfifd.3 φ _ x A
nfifd.4 φ _ x B
Assertion nfifd φ _ x if ψ A B

Proof

Step Hyp Ref Expression
1 nfifd.2 φ x ψ
2 nfifd.3 φ _ x A
3 nfifd.4 φ _ x B
4 dfif2 if ψ A B = y | y B ψ y A ψ
5 nfv y φ
6 3 nfcrd φ x y B
7 6 1 nfimd φ x y B ψ
8 2 nfcrd φ x y A
9 8 1 nfand φ x y A ψ
10 7 9 nfimd φ x y B ψ y A ψ
11 5 10 nfabdw φ _ x y | y B ψ y A ψ
12 4 11 nfcxfrd φ _ x if ψ A B