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

Metamath Proof Explorer

Theorem nfiotad

Description: Deduction version of nfiota . Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker nfiotadw when possible. (Contributed by NM, 18-Feb-2013) (New usage is discouraged.)

Ref Expression
Hypotheses nfiotad.1 ⊢ Ⅎ y φ
nfiotad.2 ⊢ φ → Ⅎ x ψ
Assertion nfiotad ⊢ φ → Ⅎ _ x ι y | ψ

Proof

Step Hyp Ref Expression
1 nfiotad.1 ⊢ Ⅎ y φ
2 nfiotad.2 ⊢ φ → Ⅎ x ψ
3 dfiota2 ⊢ ι y | ψ = ⋃ z | ∀ y ψ ↔ y = z
4 nfv ⊢ Ⅎ z φ
5 2 adantr ⊢ φ ∧ ¬ ∀ x x = y → Ⅎ x ψ
6 nfeqf1 ⊢ ¬ ∀ x x = y → Ⅎ x y = z
7 6 adantl ⊢ φ ∧ ¬ ∀ x x = y → Ⅎ x y = z
8 5 7 nfbid ⊢ φ ∧ ¬ ∀ x x = y → Ⅎ x ψ ↔ y = z
9 1 8 nfald2 ⊢ φ → Ⅎ x ∀ y ψ ↔ y = z
10 4 9 nfabd ⊢ φ → Ⅎ _ x z | ∀ y ψ ↔ y = z
11 10 nfunid ⊢ φ → Ⅎ _ x ⋃ z | ∀ y ψ ↔ y = z
12 3 11 nfcxfrd ⊢ φ → Ⅎ _ x ι y | ψ