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