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
|- F/ y ph
nfiotadw.2
|- ( ph -> F/ x ps )
Assertion nfiotadw
|- ( ph -> F/_ x ( iota y ps ) )

Proof

Step Hyp Ref Expression
1 nfiotadw.1
 |-  F/ y ph
2 nfiotadw.2
 |-  ( ph -> F/ x ps )
3 dfiota2
 |-  ( iota y ps ) = U. { z | A. y ( ps <-> y = z ) }
4 nfv
 |-  F/ z ph
5 nfvd
 |-  ( ph -> F/ x y = z )
6 2 5 nfbid
 |-  ( ph -> F/ x ( ps <-> y = z ) )
7 1 6 nfald
 |-  ( ph -> F/ x A. y ( ps <-> y = z ) )
8 4 7 nfabdw
 |-  ( ph -> F/_ x { z | A. y ( ps <-> y = z ) } )
9 8 nfunid
 |-  ( ph -> F/_ x U. { z | A. y ( ps <-> y = z ) } )
10 3 9 nfcxfrd
 |-  ( ph -> F/_ x ( iota y ps ) )