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