Metamath Proof Explorer


Theorem nfiotadw

Description: Deduction version of nfiotaw . Version of nfiotad with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 18-Feb-2013) (Revised by Gino Giotto, 26-Jan-2024)

Ref Expression
Hypotheses nfiotadw.1 y φ
nfiotadw.2 φ x ψ
Assertion nfiotadw φ _ x ι y | ψ

Proof

Step Hyp Ref Expression
1 nfiotadw.1 y φ
2 nfiotadw.2 φ x ψ
3 dfiota2 ι y | ψ = z | y ψ y = z
4 nfv z φ
5 nfvd φ x y = z
6 2 5 nfbid φ x ψ y = z
7 1 6 nfald φ x y ψ y = z
8 4 7 nfabdw φ _ x z | y ψ y = z
9 8 nfunid φ _ x z | y ψ y = z
10 3 9 nfcxfrd φ _ x ι y | ψ