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

Proof

Step Hyp Ref Expression
1 nfiotad.1
 |-  F/ y ph
2 nfiotad.2
 |-  ( ph -> F/ x ps )
3 dfiota2
 |-  ( iota y ps ) = U. { z | A. y ( ps <-> y = z ) }
4 nfv
 |-  F/ z ph
5 2 adantr
 |-  ( ( ph /\ -. A. x x = y ) -> F/ x ps )
6 nfeqf1
 |-  ( -. A. x x = y -> F/ x y = z )
7 6 adantl
 |-  ( ( ph /\ -. A. x x = y ) -> F/ x y = z )
8 5 7 nfbid
 |-  ( ( ph /\ -. A. x x = y ) -> F/ x ( ps <-> y = z ) )
9 1 8 nfald2
 |-  ( ph -> F/ x A. y ( ps <-> y = z ) )
10 4 9 nfabd
 |-  ( ph -> F/_ x { z | A. y ( ps <-> y = z ) } )
11 10 nfunid
 |-  ( ph -> F/_ x U. { z | A. y ( ps <-> y = z ) } )
12 3 11 nfcxfrd
 |-  ( ph -> F/_ x ( iota y ps ) )