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 ⊢ φ → Ⅎ 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