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